Operations Research

Motivation

In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost $k$ times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number $H(k)=1+\frac12+\dots+\frac1k$ in every directed graph, and that bound is tight for directed graphs.

For undirected graphs the paper notes that $H(k)$ is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives $H(2)=3/2$ there; Claim 4.1 improves this to $4/3$, and a three-node example shows that $4/3$ is the right value.

Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the $H(k)$ bound and the two-player undirected bound $4/3$ treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.

Setting

Let $G=(V,E)$ be a finite undirected simple graph, with a cost $c_e\ge0$ on every edge $e$. There are two players, a common terminal $s\in V$ and personal terminals $t_1,t_2\in V$. A strategy of player $i$ is a set of edges $S_i\subseteq E$ that connects $t_i$ with $s$: in the graph $(V,S_i)$, $t_i$ and $s$ lie in the same connected component. A profile is a pair $S=(S_1,S_2)$ of strategies.

Under fair cost sharing each edge is paid for equally by the players using it. With $x_e\in\{1,2\}$ the number of players whose strategy contains $e$, player $i$ pays

$$C_i(S)=\sum_{e\in S_i}\frac{c_e}{x_e}.$$

A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,

$$\mathrm{cost}(S)=\sum_{e\in S_1\cup S_2}c_e .$$

For a set $F$ of edges write $\mathrm{cost}(F)=\sum_{e\in F}c_e$. For a profile $(S_1,S_2)$, the quantities $x_1=\mathrm{cost}(S_1\setminus S_2)$, $x_2=\mathrm{cost}(S_2\setminus S_1)$ and $x_3=\mathrm{cost}(S_1\cap S_2)$ split the total cost into the private and the shared parts.

The game is an instance of a congestion game, with per-user latency $c_e/x$ on edge $e$; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.

Formalization targets

Goal: Claim 4.1 and its tightness

If the game has a profile, then some pure Nash equilibrium $S$ satisfies

$$\mathrm{cost}(S)\ \le\ \tfrac43\,\mathrm{cost}(P)\qquad\text{for every profile }P.$$

Moreover, in the three-node example (nodes $s,t_1,t_2$, edges $(s,t_1),(s,t_2)$ of cost $2$, edge $(t_1,t_2)$ of cost $1+\varepsilon$, with $0<\varepsilon<1$) the cheapest pure Nash equilibrium costs exactly $4$ and the optimum costs exactly $3+\varepsilon$, so the ratio $4/(3+\varepsilon)$ approaches $4/3$.

Milestones

1. (4.1). From every profile $(S_1,S_2)$, some pure Nash equilibrium $(S'_1,S'_2)$ has $y_1+y_2+\frac32y_3\le x_1+x_2+\frac32x_3$, where $y_i$ are the quantities of $(S'_1,S'_2)$.
2. Deviation inequalities. If $(S'_1,S'_2)$ is a Nash equilibrium and each $S_i$ is an inclusion-minimal strategy, then $y_1+\frac{y_3}2\le x_1+x_2+\frac{y_2}2+\frac{y_3}2$ and symmetrically for player 2.
3. (4.2). Under the same hypotheses, $\frac{y_1}2+\frac{y_2}2\le 2x_1+2x_2$.
4. The three-node example, as in the second half of the goal.

Significance

The result shows that the price of stability of fair cost sharing depends on the network: the $H(k)$ bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below $H(k)$ and the starting point for the later study of undirected fair network design, where the question for many players is still open.

The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.

Difficulty

The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor $H(2)=3/2$: the potential counts shared edges with weight $3/2$, so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to $4/3$ needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect $t_1$ with $t_2$, and the deviating player can then follow the other player's equilibrium route to $s$. Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.

Formalization scope

• Vertices form a Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.
• A strategy of player i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.
• The game is a CongestionGame from CongestionPoA.AsymSum.Model with latency $c_e/x$; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.
• "Price of stability at most $4/3$" is stated in existence form: some pure Nash equilibrium costs at most $\frac43$ times every profile. A formalization quantifying over all equilibria would be false (the price of anarchy is $2$), and one dropping the Nash condition would be trivial; neither is acceptable. The tightness half fixes a concrete instance and asserts both that an equilibrium of cost $4$ exists and that every equilibrium costs at least $4$.
• The deviation inequalities and (4.2) assume inclusion-minimal reference strategies; this hypothesis is implicit in the paper and does not appear in the goal, which quantifies over all profiles.

Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• G. Christodoulou, E. Koutsoupias, The price of anarchy of finite congestion games, STOC 2005, 67–73. https://doi.org/10.1145/1060590.1060600

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$-stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$, ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$, $u\in U(x)$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$. A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

$$T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),$$

and let $T^k$ be the $k$-fold composition of $T$. A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$-stage cost of $\pi$ and the $N$-stage optimal cost are

$$J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).$$

A policy is uniformly $N$-stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$-stage optimal, and $N$-stage $\varepsilon$-optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$.

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$), and F.3 (a quantitative selection property with a constant $\beta>0$).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$:

$$J^*_N=T^N(J_0),$$

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$.

Milestones

• Proposition 3.3: $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$. Needs monotonicity only.
• Corollary 3.3.1: a uniformly $N$-stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$.
• Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy exists.
• Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$.
• Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$.
• Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$, $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$, policies with $\{\varepsilon_n\}$-dominated convergence to optimality exist.
• Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$, the DP algorithm gives $J^*_N$ and $N$-stage $\varepsilon$-optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$. Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$. The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$-optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$, which is why F.3 and the definition of $\varepsilon$-optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$. Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$.

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$, so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate $\lambda$, service times are exponential with mean $1/\mu$, and $N$ agents serve in parallel. Practitioners use the square-root safety staffing rule $N \approx \lambda/\mu + y\sqrt{\lambda/\mu}$, which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from $0$ and $1$.

Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.

Setting

Fix a service rate $\mu > 0$. For every arrival rate $\lambda > 0$ a waiting-cost function $D_\lambda$ assigns cost $D_\lambda(t)$ to a wait of $t$ time units; it satisfies $D_\lambda(0) = 0$, is strictly increasing, and $t \mapsto D_\lambda(t)e^{-\theta t}$ is integrable on $(0,\infty)$ for every $\theta > 0$. A staffing cost $F$, defined for real $N > 0$, is convex and strictly increasing.

For an integer $N > \lambda/\mu$ the probability of waiting is the Erlang-C formula

$$\pi(N,\nu) = \frac{\nu^N}{N!}\Bigl\{(1-\nu/N)\sum_{n=0}^{N-1}\frac{\nu^n}{n!} + \frac{\nu^N}{N!}\Bigr\}^{-1},\qquad \nu = \lambda/\mu,$$

the expected waiting cost of a delayed customer is $G(N,\lambda) = (N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt$, and the total cost per unit time is $C(N,\lambda) = F(N) + \lambda\,\pi(N,\lambda/\mu)\,G(N,\lambda)$. An optimal staffing level $N^*_\lambda$ minimizes $C(\cdot,\lambda)$ over the integers $N > \lambda/\mu$.

Write $N_\lambda(x) = \lambda/\mu + x\sqrt{\lambda/\mu}$, and for $x > 0$ put $F_\lambda(x) = F(N_\lambda(x)) - F(\lambda/\mu)$, $G_\lambda(x) = \lambda G(N_\lambda(x),\lambda)$, and $\pi_\lambda(x) = H(N_\lambda(x),\lambda/\mu)$, where $H(M,\alpha) = \{\alpha\int_0^\infty e^{-\alpha t}t(1+t)^{M-1}dt\}^{-1}$ extends the Erlang-C formula to real $M$. The normalized cost is $C_\lambda(x) = F_\lambda(x) + \pi_\lambda(x)G_\lambda(x)$, and a surrogate cost is $C[z;\hat F,\hat\pi,\hat G] = \hat F(z) + \hat\pi(z)\hat G(z)$. Rounding is measured by $S_\lambda(x) = \min\{C(\lfloor N_\lambda(x)\rfloor,\lambda), C(\lceil N_\lambda(x)\rceil,\lambda)\}$.

Two special functions appear. The Halfin–Whitt delay function is $P(x) = 1/(1 + x/h(-x))$ with $h = \phi/(1-\Phi)$ the standard normal hazard rate. The Stirling-type approximation is

$$Q_\lambda(x) = \frac{\exp\{N_\lambda(x)[1 - r_\lambda(x) + \log r_\lambda(x)]\}}{\sqrt{2\pi N_\lambda(x)}\,(1-r_\lambda(x))},\qquad r_\lambda(x) = \frac{\lambda/\mu}{N_\lambda(x)}.$$

Asymptotic relations are limits of ratios as $\lambda\to\infty$: $a_\lambda \stackrel{\infty}{\approx} b_\lambda$ means $a_\lambda/b_\lambda \to 1$, and $a_\lambda \stackrel{\infty}{\ll} b_\lambda$ means $a_\lambda/b_\lambda \to 0$.

Formalization targets

Goal: Theorem 7.1

Assume the regime is quality-driven, display (27): $F_\lambda(\kappa) \stackrel{\infty}{\ll} G_\lambda(\kappa)$ for every $\kappa > 0$. Let $y^*_\lambda$ minimize $F_\lambda(y) + Q_\lambda(y)G_\lambda(y)$ over $y > 0$. Then

$$\lim_{\lambda\to\infty}\frac{S_\lambda(y^*_\lambda) - F(\lambda/\mu)}{C(N^*_\lambda,\lambda) - F(\lambda/\mu)} = 1.$$

The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.

Milestones

In attack order: Lemma C.1 ($G_\lambda$ strictly convex decreasing); the identity $H(N,\nu) = \pi(N,\nu)$ at integer $N$ (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ($P$ strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, $\pi_\lambda(x_\lambda) \stackrel{\infty}{\approx} Q_\lambda(x_\lambda)$ whenever $x_\lambda\to\infty$.

Significance

Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function $P$ is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows $\sqrt{\lambda/\mu}$ and $P$ must be replaced by the Stirling-type expression $Q_\lambda$. The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over $N$ into a smooth problem, and it marks the boundary of validity of square-root staffing.

The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of $G_\lambda$ and of $P$, the Halfin–Whitt limit for the continuous extension $\pi_\lambda$, and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.

Difficulty

The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of $\pi_\lambda$ at a staffing excess $x_\lambda$ that may grow at any rate, from barely faster than a constant to faster than $\sqrt{\lambda}$, where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension $\pi_\lambda$ at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum $x^*_\lambda$ or the surrogate optimum $y^*_\lambda$ says that they do.

Formalization scope

Lean represents $\lambda$ as a positive real, and $\lambda\to\infty$ is the filter atTop on $\mathbb{R}$ with $\mu$ fixed. The standing assumptions on $\mu$ and $D_\lambda$ are the structure WaitModel; $F$ is a function argument with hypotheses ConvexOn and StrictMonoOn on $(0,\infty)$. Staffing levels $N$ are natural numbers. Minimizers ($N^*_\lambda$, $x^*_\lambda$, $z^*_\lambda$, $y^*_\lambda$) are function arguments with minimality hypotheses at every $\lambda > 0$, so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.

The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost $C(N,\lambda)$ with the Erlang-C formula.

Conventions committed to: (i) the goal adds the hypothesis $G(N,\lambda)\to\infty$ as $N\downarrow\lambda/\mu$, which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when $D_\lambda$ is unbounded); (ii) in $S_\lambda$ the floor term is omitted when $\lfloor N_\lambda(x)\rfloor \le \lambda/\mu$, since the cost is undefined at unstable levels; (iii) the integrability of $D_\lambda(t)e^{-\theta t}$ is explicit, because a Lean integral of a non-integrable function is $0$; (iv) $P(0) = 1$, the value of formula (11) at $0$; (v) display (15) is stated for $b > 0$, since the ratio $a_\lambda/b$ is undefined at $b = 0$. The instance $\mu = 1$, $F(N) = cN$, $D_\lambda(t) = a\sqrt{\lambda}\,t$ (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking $\pi_\lambda$ or $G_\lambda$ at Lean default values is ruled out by these explicit domain conditions.

Only the first statement of Lemma 4.2 is a milestone: the second, $\pi_\lambda(x_\lambda)\approx Q(x_\lambda)$ under $x_\lambda \stackrel{\sup}{\le} \lambda^{1/6}$, fails as printed at $x_\lambda = \lambda^{1/6}$. Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.

Selected references

• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000 (the version formalized here; every index and page cited in this mission is the report's).
• S. Borst, A. Mandelbaum, M. I. Reiman, Dimensioning Large Call Centers, Operations Research 52(1):17–34, 2004. https://doi.org/10.1287/opre.1030.0081
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
• N. Gans, G. Koole, A. Mandelbaum, Telephone Call Centers: Tutorial, Review, and Research Prospects, Manufacturing & Service Operations Management 5(2):79–141, 2003. https://doi.org/10.1287/msom.5.2.79.16071

Motivation

Many large convex programs have the form "minimize a strictly convex function $f$ subject to linear equations $Ax=b$". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When $A$ is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of $A$.

L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets $A_i$, in which each step replaces the current point by its $D$-projection onto one set: the minimizer of a distance-like function $D(\cdot,y)$ over that set. §2 chooses $D$ from the objective $f$ itself, $D(x,y)=f(x)-f(y)-(g(y),x-y)$ with $g$ the gradient of $f$; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes $f$ over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.

Setting

Work in the Euclidean space $E^p$ with inner product $(\cdot,\cdot)$. Let $S\subset E^p$ be a convex set with closure $\bar S$ and interior $\operatorname{int}S$. Let $f$ be strictly convex and continuously differentiable over $S$, with gradient $g(x)$ at $x\in S$, and continuous over $\bar S$. Let $A$ be an $m\times p$ matrix with nonzero rows $A_1,\dots,A_m$ and $b\in E^m$. The problem (2.1)–(2.3) is

$$\text{minimize } f(x)\quad\text{subject to}\quad Ax=b,\ x\in\bar S,$$

with feasible set $R=\{x\in E^p\mid Ax=b,\ x\in\bar S\}$, assumed nonempty. A point of $R$ minimizing $f$ over $R$ is a solution.

The function (1.4) is

$$D(x,y)=f(x)-f(y)-\bigl(g(y),x-y\bigr),$$

and $A_i$ also denotes the hyperplane $\{x\mid (A_i,x)=b_i\}$. The paper assumes that $D$ satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every $y\in S$, a $D$-projection $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$. It also assumes condition (2): if $y^n\in S$ and $y^n\to y^*\in\bar S$, then $D(y^*,y^n)\to 0$.

A relaxation sequence with control $(i_n)_{n\ge0}$ starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. The control is any sequence of row indices. Finally,

$$Z=\{x\in S\mid g(x)=uA=\textstyle\sum_i u_iA_i\ \text{for some } u\in E^m\}$$

is the set of points of $S$ at which the gradient lies in the row space of $A$.

Formalization targets

Goal: Theorem 3

Assume that the $D$-projection of every point of $\operatorname{int}S$ onto every $A_i$ lies in $\operatorname{int}S$. For every control and every relaxation sequence with $x^0\in Z\cap\operatorname{int}S$ that converges to a point $x^*\in R$,

$$f(x^*)\le f(y)\qquad\text{for every } y\in R .$$

Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.

Milestones

1. Lemma 3. If $y^*\in R\cap\bar Z$, then $y^*$ is a solution of (2.1)–(2.3).
2. (2.7)–(2.8). For $x\in\operatorname{int}S$ there is $\lambda\in\mathbb R$ with $g(P_ix)=g(x)+\lambda A_i$ and $(A_i,P_ix)=b_i$.
3. Invariance of $Z$. $P_i$ maps $Z\cap\operatorname{int}S$ into $Z\cap\operatorname{int}S$.

An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.

Significance

Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier $\lambda$ of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for $f(x)=\tfrac12\|x\|^2$.

The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.

Difficulty

The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of $A$, so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on $S$, the limit may lie on the boundary of $S$ (or outside $S$, in $\bar S$), and $g$ need not extend continuously there, so the multipliers $u^n$ need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at $y^*$. Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that $P_i$ preserves $\operatorname{int}S$; on the boundary of $S$ a minimizer over $A_i\cap S$ need not satisfy (2.7).

Formalization scope

The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and $(A_i,x)$ is the real inner product. The gradient $g$ is explicit data tied to $f$ by HasGradientWithinAt f (g x) S x for $x\in S$ and continuous on $S$; $S$ is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:

• The $D$-projection is a fixed map $P$; condition II says $P_iy$ minimizes $D(\cdot,y)$ over $A_i\cap S$, and condition III is stated for that map.
• Condition IV is assumed in its one-sided directional form (implied by the paper's), so theorems under it are at least as strong as the paper's.
• "Compact" in conditions V and VI is sequential compactness. Condition V is assumed for the points of $R\cap S$.
• Condition (2) is assumed for limits $y^*\in\bar S$; the page prints $y^*\in S$, but its use at a feasible point needs $\bar S$.
• Translation slips are corrected in the statements and recorded: condition II's "$D(z,x)$" and "$i\in T$", (2.7)'s "$g(x^{n-1})$" (read $g(x^{n+1})$), and "Theorems 1 − 3" (read Theorems 1–2).
• The control is an arbitrary sequence of indices in $\{0,\dots,m-1\}$; λ is named lam.
• Note 2 is stated for candidate points $y,z\in S$, where $g$ is meaningful.

The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open $S$, or to a limit assumed to lie in $Z$: any of these would trivialize the passage to the limit that the theorem is about.

A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality $f(x)\ge f(y)+(g(y),x-y)$ for $x\in\bar S$, $y\in S$, and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Comput. Math. Math. Phys. 7(3) (1967) 200–217. doi:10.1016/0041-5553(67)90040-7
• Y. Censor, S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997. doi:10.1093/oso/9780195100624.001.0001
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, J. Optim. Theory Appl. 34 (1981) 321–353. doi:10.1007/BF00934676

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$, the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$. Let $D_\lambda(t)$ be the cost of a wait of length $t$. It is strictly increasing on $t\ge0$, satisfies $D_\lambda(0)=0$, and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

$$G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.$$

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$. Total cost per unit of time at a stable integer level is

$$C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).$$

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$, define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$, $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$, and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$. The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$. These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

$$\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.$$

For each $\lambda>0$, choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$. Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

$$\lim_{\lambda\to\infty} \frac{S_\lambda(y^*_\lambda)-F(\lambda/\mu)} {C(N^*_\lambda,\lambda)-F(\lambda/\mu)}=1.$$

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$, which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$. Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$, its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$, $\mu$, offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$. Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$.

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$, although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$, unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

• Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

Motivation

In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.

Section 6 of the same paper turns to weighted players: player $i$ has a weight $w_i \ge 1$ (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.

Setting

A finite directed multigraph $D$ has a finite set $E$ of arcs; each arc $e$ has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source $s$ and a sink $t$. A simple $s$–$t$ path is a sequence of arcs $e_1,\dots,e_m$ ($m\ge1$), each starting where the previous one ends, beginning at $s$, ending at $t$, and visiting no vertex twice; it is identified with its arc set $P\subseteq E$. Write $\mathcal S_{st}$ for the finite set of these paths.

The weighted single-commodity game has a finite set of players; player $i$ has a weight $w_i\ge1$, arc $e$ has a fixed cost $c_e\ge0$, and every player's strategy set is $\mathcal S_{st}$. In a profile $S=(S_i)_i$ let

$$W_e=\sum_{i\,:\,e\in S_i} w_i$$

be the total weight on arc $e$. Player $i$ pays

$$\mathrm{pay}_i(S)=\sum_{e\in S_i}\frac{w_i}{W_e}\,c_e .$$

A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.

A best-response move of player $i$ replaces $S_i$ by a path $T$ that minimises $i$'s payment given the other players' paths, provided this strictly lowers $i$'s payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.

Formalization targets

Goal: Theorem 6.3 (p. 1620)

For every such game with $w_i\ge1$ and $c_e\ge0$:

$$\text{there is no infinite sequence } S^0,S^1,\dots \text{ with } S^{n+1} \text{ a best-response move from } S^n;$$ $$\text{a profile admitting no best-response move is a Nash equilibrium;}$$ $$\mathcal S_{st}\neq\emptyset \;\Longrightarrow\; \text{a pure Nash equilibrium exists.}$$

The goal asserts only termination and existence; it fixes no bound on the length of a run.

Milestones (proof of Theorem 6.3, p. 1620)

For a profile $S$ define the marginal cost of a path, $c_S(P)=\sum_{e\in P}c_e/W_e\in[0,+\infty]$, and the tuple $P(S)$ of all values $c_S(P)$, $P\in\mathcal S_{st}$, sorted increasingly. With strictly positive arc costs:

1. a player on path $P$ pays $w_i\,c_S(P)$ (this one needs only $c_e\ge0$);
2. inequality (6.1): if player $i$ makes a best-response move from $P_1$ to $P_2$ and $\mathcal P$ is the set of paths sharing an arc with $P_1\cup P_2$, then $\min_{P\in\mathcal P}c_{S'}(P)<\min_{P\in\mathcal P}c_S(P)$;
3. every best-response move strictly decreases $P(S)$ in the lexicographic order.

Significance

The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.

The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.

Difficulty

The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential $\Phi$ is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.

The argument also depends on the shape of the strategy sets. Two distinct simple $s$–$t$ paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: $c_e/W_e$ is $0/0$ on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.

Formalization scope

• Players form a finite type; arcs form a finite type with tail and head maps into a vertex type. Parallel arcs are kept.
• A strategy is a Finset of arcs; the strategy family of every player is the finite set of arc sets of simple $s$–$t$ paths (a list of consecutive arcs with distinct visited vertices). There are no paths when $s=t$.
• Weights and costs are real numbers with $w_i\ge1$, $c_e\ge0$ (the predicate IsStandard); the milestones (6.1) and the lexicographic decrease assume $c_e>0$.
• Payments are real; on every used arc $W_e\ge w_i\ge1$, so the division is never by zero.
• The marginal cost $c_S(P)$ is valued in $[0,+\infty]$ (ℝ≥0∞): an unused arc of positive cost contributes $+\infty$. Computing it in the reals, where $x/0=0$, would make unused paths free and the milestones false.
• Termination is the well-foundedness of the relation "$S'$ is reached from $S$ by one best-response move" with $S'$ below $S$; the reverse orientation is a different statement.
• A best-response move requires a strict improvement and an exact minimiser; dropping either makes termination trivially true or false, and the second clause of the goal (no move possible implies Nash) guards against a move relation that is too narrow.

Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games and Economic Behavior 14:124–143, 1996. https://doi.org/10.1006/game.1996.0044
• H. Chen, T. Roughgarden, Network design with weighted players, Proceedings of the 18th ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), 2006, pp. 28–37.

Motivation

Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.

Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting $O(n^2)$ procedure is the standard algorithm for the problem written $1\,|\,\mathrm{prec}\,|\,f_{\max}$ in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.

Setting

A finite, nonempty set $J$ of jobs is processed on a single machine, one job at a time and without interruption. Each job $j$ has a processing time $a_j \ge 0$ and a cost function $c_j : \mathbb{R} \to \mathbb{R}$ that is monotone nondecreasing. The value $c_j(t)$ is the cost incurred when $j$ is completed at time $t$.

The precedence constraints are an arbitrary relation $\prec$ on jobs: $i \prec j$ means that job $i$ is required to precede job $j$. A sequence $\pi = (\pi_1, \dots, \pi_n)$ lists every job of $J$ once. It observes the precedence constraints if $\pi_q \prec \pi_p$ never holds for positions $p < q$. The machine starts at time $0$ with no idle time, so the completion time of $\pi_m$ is $C_{\pi_m}(\pi) = a_{\pi_1} + \dots + a_{\pi_m}$. The maximum incurred cost of $\pi$ is

$$f_{\max}(\pi) = \max_{j \in J} c_j\bigl(C_j(\pi)\bigr),$$

and a feasible $\pi$ is minmax optimal if $f_{\max}(\pi) \le f_{\max}(\pi')$ for every feasible $\pi'$.

For a set $P$ of jobs, $S(P)$ is the set of jobs of $P$ that are not required to precede any other job of $P$, and $T_P = \sum_{j \in P} a_j$. Lawler's rule builds a sequence from the last position to the first. With $P$ the jobs not yet placed, it chooses $k \in S(P)$ with $c_k(T_P) = \min_{j \in S(P)} c_j(T_P)$, places $k$ in the latest open position and removes it from $P$. Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible ($S$), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.

Formalization targets

Goal: the rule is optimal

Every sequence $\pi$ that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies

$$f_{\max}(\pi) \;\le\; f_{\max}(\pi') \qquad \text{for every sequence } \pi' \text{ of } J \text{ observing the precedence constraints.}$$

This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.

Milestones

1. §2 proof, third paragraph. Moving a job of $S(J)$ to the end of a feasible sequence keeps it feasible.
2. §2 proof, fourth paragraph, first sentence. After that move, no job other than $k$ completes later, and $k$ completes at $T = \sum_{j \in J} a_j$.
3. §2 proof, fourth paragraph. If $c_k(T) \le c_{k'}(T)$, where $k'$ is the last job of the feasible sequence, the move does not raise $f_{\max}$.
4. THEOREM (§2), p. 544. If some feasible sequence exists and $k \in S(J)$ minimizes $c_j(T)$ over $S(J)$, then some minmax optimal sequence has $k$ last.
5. §3, the reduction. A minmax optimal sequence of $J \setminus \{k\}$, followed by $k$, is minmax optimal for $J$.
6. §3, the procedure never stalls. If a feasible sequence exists, the rule produces a complete sequence. This shows the goal is not vacuous.

Significance

The result shows that $1\,|\,\mathrm{prec}\,|\,f_{\max}$ is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the $n$ partial sums $T_P$ along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for $f_{\max}$ objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.

The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets $S(P)$ and times $T_P$ to be the correct ones at each stage, which the definitions fix.

Difficulty

The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set $S(P)$ and the time $T_P$ must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.

A first attempt often proves only the Theorem, that some optimal sequence has $k$ last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of $J$ with $k$ last need not restrict to an optimal sequence of $J \setminus \{k\}$. Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.

Formalization scope

• Jobs form a type ι with decidable equality, and the job set is J : Finset ι.
• Processing times are a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.
• A sequence is a duplicate-free list whose elements are exactly J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).
• The relation prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in $S$ (the "others" of the page exclude the job itself).

The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing $c_j$ for $j \in J$, and $J$ nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative ($a_j \ge 0$), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.

The rule is the property IsLawlerSequence of a finished sequence. At each position $m$, the job there lies in $S$ of the jobs in positions $0..m$ and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.

The $n^2$ operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.

Selected references

• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• E. L. Lawler and J. M. Moore, A Functional Equation and its Application to Resource Allocation and Sequencing Problems, Management Science 16(1):77–84, 1969. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• R. L. Graham, E. L. Lawler, J. K. Lenstra and A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: a Survey, Annals of Discrete Mathematics 5:287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X