Operations Research

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$. Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$, the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$, chooses $x\in B$. For every $s$ and possible $B$, $x\mapsto P(x\mid s,B)$ is a probability vector on $B$. Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

• Axiom 1 (IIA). For all possible $B$, all $s$ and all $x,y\in B$: $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$.
• Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$, all $s$, all $x\in B$.
• Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$, and $p_{xx}=\tfrac12$ by definition.
• The function $V$. $V(s,x,z)=\log(p_{xz}/p_{zx})$.
• Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$, with $v(s,x)=V(s,x,z)$, for every $s$, every possible $B$ (containing $z$ or not) and every $x\in B$:

$$P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.$$

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

1. Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$, Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$.
2. Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$.
3. Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$.
4. Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
5. Equation (10): for a benchmark $z\in B$, $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$.

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$. The goal requires a single $v$ for all sets, including sets that do not contain $z$, where neither Equation (10) nor the axioms on $B$ alone say anything about $z$. A second subtlety is the diagonal: $\{x,x\}=\{x\}$, so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$, never as "for each $B$ there is a $v$", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$. Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$, a randomized local search achieving $2/5$, and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$.
• Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$-approximation (this mission) and a randomized linear-time $1/2$-approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$, and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$. In iteration $i = 1, \dots, n$ it computes

$$a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).$$

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$, $Y_i = Y_{i-1}$; otherwise $X_i = X_{i-1}$, $Y_i = Y_{i-1} \setminus \{u_i\}$. A tie adds $u_i$. After $n$ iterations $X_n = Y_n$, which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$, which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$. In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$,

$$X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).$$

Milestones

1. Lemma II.1. For every $1 \le i \le n$, $a_i + b_i \ge 0$.
2. The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$.
3. Lemma II.2. For every $1 \le i \le n$,

$$f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].$$

4. The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$.
5. Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$.

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$, is the template the paper then refines into the randomized $1/2$-approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$, which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$, not against $OPT$. For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

• The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
• Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
• The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$.
• The tie rule is line 5's $a_i \ge b_i$: ties add $u_i$.
• Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
• The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$, because $f(OPT)$ may be $0$.
• Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$-approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$, without which $f \equiv 0$ would satisfy it.
• Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$. A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$" would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$, independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$. The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$, $\alpha\ge0$.

The state at the start of a period is $(x_1,w_1,x_2)$: $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$. Installation 1 pays the expected holding and shortage cost (1),

$$L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}$$

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$,

$$C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)$$

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$, $\hat C_0\equiv0$:

$$\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)$$

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$,

$$C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)$$

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$, as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

1. Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
2. The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$, with $f_n$ of (7) (p. 480).
3. Convexity of every $f_n$ (§2 item 3, p. 478).
4. Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$.
5. Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

$$\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.$$

6. Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$.

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$. When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$. The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$. Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$. On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$. Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

• The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$; $\varphi\ge0$ with $\int_0^\infty\varphi=1$; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$, no convexity of $\tilde L$, no $K=0$ and no sign condition on $w_1$ is assumed.
• Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
• Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$; outside it the feasible set of (14) is empty.
• The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$, and $f_n\equiv0$ for $n\le2$.

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$, and of any milestone are welcome.

Selected references

• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

Motivation

Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.

The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.

Setting

A directed network has $n$ numbered points. Its length matrix $w$ assigns a real number $w(i,j)$ to a direct link from $i$ to $j$. The value $\infty$ means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries $w(i,i)$ are unrestricted. The paper's matrix index range is $1,\ldots,n$; the Lean development uses $0,\ldots,n-1$ in the same order.

A path from $i$ to $j$ is a sequence $p_0=i,p_1,\ldots,p_L=j$ with $L\ge1$ links. The points $p_0,\ldots,p_{L-1}$ are distinct, as are $p_1,\ldots,p_L$. Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is $\ell_w(p)=\sum_{t=0}^{L-1}w(p_t,p_{t+1})$; a missing link gives length $\infty$. Write $d_w(i,j)$ for the minimum length among these paths, taking $d_w(i,j)=\infty$ when there is no finite-length path. Since $L\le n$, this is a minimum over a finite family.

The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.

Algorithm 97 scans a pivot $i$, then row $j$, then column $k$, each in increasing order. It enters the column scan when the current $m(j,i)$ is finite; if the current $m(i,k)$ is also finite, it computes $s=m(j,i)+m(i,k)$ and replaces $m(j,k)$ when $s<m(j,k)$. Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when $m(j,i)$ and $m(i,k)$ are true, it sets $m(j,k)$ to true.

Formalization targets

Reachability and missing paths

For Algorithm 96, let $b^+$ be the transitive closure of the initial parent relation $b$, using chains of one or more links. Its comment asserts

$$\operatorname{ancestor}(b)(i,j)=\mathrm{true}\quad\Longleftrightarrow\quad i\mathrel{b^+}j.$$

For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from $i$ to $j$,

$$\operatorname{shortestPath}(w)(i,j)=\infty.$$

This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.

Complete shortest-path matrix

The goal is the whole output claim of Algorithm 97. For every $n$, every matrix $w$ with no negative cycle, and all points $i,j$,

$$\operatorname{shortestPath}(w)(i,j)=d_w(i,j).$$

The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.

Significance

The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.

Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.

Difficulty

The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on $m(j,i)$ is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.

Formalization scope

Points are Fin n, including the empty network at $n=0$ and the single-point network at $n=1$. Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is $10^{10}$; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.

The initial diagonal is not normalized. Therefore a path from $i$ to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.

The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length $-1$, the procedure changes that entry to $-2$, although the shortest simple closed path has length $-1$. No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark $d_w$ is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.

Selected references

• Robert W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6), 1962, p. 345. DOI 10.1145/367766.368168.
• Robert W. Floyd, Algorithm 96: Ancestor, Communications of the ACM 5(6), 1962, pp. 344–345, in the same published Algorithms department scan.

Motivation

Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.

The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.

Timeline, as far as it bears on this mission:

• 1960: Manne, Linear Programming and Sequential Decisions, shows that linear programming applies to the average-cost problem, in the context of an inventory problem; Wagner, On the Optimality of Pure Strategies, shows by linear programming that a deterministic stationary procedure is optimal for it.
• 1960: Howard, Dynamic Programming and Markov Processes, gives policy iteration for the average-cost problem over stationary procedures.
• 1962: Derman proves that a deterministic stationary procedure is optimal over all procedures for the average-cost criterion (Theorem 1), formulates the average and total cost problems as linear programs under irreducibility assumptions (Theorem 2), and extends the optimality of deterministic stationary procedures to the ratio criterion (Theorem 3).
• 1962: Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, gives a problem of the ratio type (cited by Derman, p. 18).
• 1963: Jewell, Markov-renewal programming, treats the gain rate (reward per unit sojourn time) of semi-Markov decision processes, over stationary policies.

Setting

A system is observed at times $t = 0, 1, \dots$ in one of finitely many states $0, \dots, L$. After each observation one of the decisions $d_1, \dots, d_K$ is made, all of them available in every state. If the system is in state $i$ and decision $d_k$ is made, the next state is $j$ with probability $q_{ij}(k) \ge 0$, where $\sum_j q_{ij}(k) = 1$.

A procedure $R$ chooses the decision at time $t$ at random, with probabilities $D_k(X_0, \Delta_0, \dots, X_t)$ that may depend on the whole past; the class of all procedures is $C$. The class $C'$ consists of the stationary randomized procedures, for which the probability of $d_k$ in state $i$ is a fixed number $D_{ik}$, whatever the past and the time. The class $C''$ consists of the deterministic stationary procedures, those of $C'$ with every $D_{ik} \in \{0, 1\}$; it is finite. A procedure of $C'$ turns the states into a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$.

Let $w'_{ik} > 0$ and $w''_{ik} > 0$ be two sets of costs incurred when decision $d_k$ is made in state $i$. For a fixed procedure $R$ started at $X_0 = i$, let $W'_t$ and $W''_t$ be the expected costs at time $t$. The ratio criterion is

$$\psi_R(i) = \limsup_{T\to\infty} \frac{\sum_{t=0}^{T} W'_t}{\sum_{t=0}^{T} W''_t}.$$

For a single cost set $w$ with expected costs $W_t$, the average cost per unit time is $Q_R(i) = \limsup_{T\to\infty} \frac1T \sum_{t=0}^{T} W_t$.

Assumption A says that for every procedure of $C'$ all states $0, \dots, L$ belong to the same class of the induced Markov chain.

Formalization targets

Goal: Theorem 3 (p. 23)

Under Assumption A, for every initial state $i$ there is a deterministic stationary procedure $R_3 \in C''$ with

$$\psi_{R_3}(i) = \min_{R \in C} \psi_R(i),$$

that is, $\psi_{R_3}(i) \le \psi_R(i)$ for every procedure $R \in C$.

Steps of the proof (milestones)

1. Theorem 1 (1) for costs of either sign: for every real cost $w$ there is $R_1 \in C''$ with $Q_{R_1}(i) \le Q_R(i)$ for all $R \in C$ and all $i$.
2. For any procedure $R$, $\psi_R(i) \le m$ implies $Q_R(i) \le 0$ for the costs $w_{ik} = w'_{ik} - m\, w''_{ik}$.
3. Under Assumption A, for $R^* \in C''$, $Q_{R^*}(i) \le 0$ for those costs implies $\psi_{R^*}(i) \le m$.
4. For $R \in C'$ under Assumption A, $\psi_R(i) = \dfrac{\sum_{s}\sum_k \pi_s D_{sk} w'_{sk}}{\sum_s\sum_k \pi_s D_{sk} w''_{sk}}$, with $\pi$ the stationary distribution of $(p_{sj})$.

Significance

Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing $w' - m w''$ and adjusting $m$, underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.

All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.

Difficulty

The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages $\frac1T\sum_{t\le T} W'_t$ and $\frac1T\sum_{t \le T} W''_t$ need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.

Formalization scope

The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class $C$ is Policy M, history-dependent and randomized; $C''$ is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs $w'$, $w''$ and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.

The local definitions are: the expected cost at time $t$ for a real cost, as a finite sum over histories of length $t+1$; $Q_R(i)$ with Derman's normalization ($T+1$ terms divided by $T$); $\psi_R(i)$ as the limit superior of the ratio of partial sums; the induced matrix $p_{ij}$; Assumption A as Matrix.IsIrreducible of $p$ for every row-stochastic $D \ge 0$; and membership of a procedure in $C'$ with probabilities $D$. All limits superior are real, of bounded sequences; positivity of $w'$ and $w''$ is a hypothesis of every statement involving $\psi$, which keeps the denominators positive.

The goal quantifies "for every initial state there is $R_3$", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.

Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class $C''$.

Selected references

• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• M. Klein, Inspection-Maintenance-Replacement Schedules Under Markovian Deterioration, Management Science 9(1), 1962.
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 1960.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6):938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037

Motivation

Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.

The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of $Jm_2+1$ iterations quoted below. This mission formalizes that section.

Setting

First-stage data are $c\in\mathbb R^{n_1}$, $A\in\mathbb R^{m_1\times n_1}$, $b\in\mathbb R^{m_1}$, and the first-stage feasible set is $K_1=\{x\mid Ax=b,\ x\ge0\}$. A deterministic technology matrix $T\in\mathbb R^{m_2\times n_1}$, with rows $T_i$, maps $x$ to the tender $\chi=Tx\in\mathbb R^{m_2}$. Problem (3) of the paper is

$$\min\ z(x)=cx+\Psi(Tx)\quad\text{s.t. } x\in K_1 .$$

For each row $i=1,\dots,m_2$ the random vector $\xi_i=(q_i^+,q_i^-,h_i)$ takes $J$ values $\xi_{ij}=(q^+_{ij},q^-_{ij},h_{ij})$ with probabilities $p_{ij}$. The simple recourse cost (20) of row $i$ is the optimal value of a one-row LP,

$$\psi_i(\chi_i,\xi_{ij})=\min\{q^+_{ij}y^+ + q^-_{ij}y^- \mid y^+-y^-=h_{ij}-\chi_i,\ y^+,y^-\ge0\},$$

and by separability (19) the expected recourse function is $\Psi(\chi)=\sum_i\Psi_i(\chi_i)$ with $\Psi_i(\chi_i)=\sum_j p_{ij}\psi_i(\chi_i,\xi_{ij})$. Write $q_{ij}=q^+_{ij}+q^-_{ij}$.

The multicut algorithm for simple recourse problems (p. 389) keeps a set $I$ of identified pairs $l=(i,j)$, initially empty. Step 1 solves the master program (26),

$$\min\ cx+\sum_{i,j}p_{ij}q^-_{ij}(T_ix)+\sum_{l\in I}u_l\quad\text{s.t. } Ax=b,\ x\ge0,\ u_l\ge e_l-E_lx,\ u_l\ge0\ (l\in I),$$

with $E_l=p_{ij}q_{ij}T_i$ and $e_l=p_{ij}q_{ij}h_{ij}$. Step 2 adds to $I$ every pair for which the constraint $0\ge p_{ij}q_{ij}(h_{ij}-T_ix^\nu)$ (27) is violated at the master's solution $x^\nu$, and returns to Step 1; when no pair is added the algorithm stops.

Formalization targets

Goal: the $Jm_2+1$ bound, with correctness

The paper states (p. 389): "The initial problem (26) involves $m_1$ constraints and $n_1$ variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is $Jm_2+1$." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):

$$\nu\text{-th solve of Step 1 takes place}\ \Longrightarrow\ \nu\le Jm_2+1,$$

and, when the algorithm stops at $x^\nu$, $x^\nu\in K_1$ and $cx^\nu+\Psi(Tx^\nu)\le cx+\Psi(Tx)$ for all $x\in K_1$.

Milestones

1. (22)–(23): for $q^++q^-\ge0$ the LP (20) attains its minimum $\max\{q^-(\chi-h),q^+(h-\chi)\}$, so each $\theta_{ij}$ has only two cuts.
2. (24)–(25): the simple recourse problem is equivalent to the LP (25): same optimal $x$, and the value of (25) at $x$ with the best slacks is $z(x)$.
3. Relaxation and stopping: (26) is a relaxation of (25), and if no unidentified pair violates (27) at an optimum of (26), that optimum (extended by zero slacks) is optimal for (25).
4. Facets: each $\Psi_i$ is a maximum of $J+1$ affine functions, so $\Psi$ is a maximum of at most $(J+1)^{m_2}$ affine functions.

Significance

The bound is linear in $m_2$ and $J$, while the L-shaped method may need as many iterations as $\Psi$ has facets, up to $(J+1)^{m_2}$ (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in $m_2J$, a fact used throughout the later literature on simple and integrated recourse.

The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.

Difficulty

The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of $J$ convex functions, each with one breakpoint, is a maximum of exactly $J+1$ affine functions, which is not a consequence of convexity alone.

Formalization scope

All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs $(i,j)$ by Fin m2 × Fin J. The second-stage value $\psi$ is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by $p_{ij}\ge0$ with $\sum_jp_{ij}=1$.

Readings pinned down, each recorded in the item statements:

• $q_{ij}\ge0$. The paper never states it, but without it (20) is unbounded below and (25) is not equivalent to (3). It is a field of the model.
• $x\ge0$ belongs to (3) and is omitted in the displays of (25) and (26); it is kept in both.
• Step 2 ranges over unidentified pairs. The paper writes "for each $i$ and $j$"; read literally, an identified pair whose $u_l$ already covers it could be re-added forever. The paper's remark that (27) "identifies any constraints in (25) that are not met" fixes the reading. The state of the algorithm is the set of identified pairs; the order of identification, and so the index $t$, is immaterial.
• Stopping rule. It is implicit in the paper: stop when (27) is violated for no pair.
• Counting. The paper writes "the maximal number of iterations is $Jm_2+1$"; we count solves of Step 1, the stopping solve included, which is what its argument counts.
• Constant. The objective of (26) omits the constant $-\sum p_{ij}q^-_{ij}h_{ij}$ of (25), as printed.
• Facets. "$\Psi_i$ contains $J+1$ facets" is read as "is a maximum of $J+1$ (not necessarily distinct) affine functions".

A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.

Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on $\mathbb R$. Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.

Selected references

• J.R. Birge and F.V. Louveaux, A multicut algorithm for two-stage stochastic linear programs, European Journal of Operational Research 34 (1988) 384–392. https://doi.org/10.1016/0377-2217(88)90159-2
• R.M. Van Slyke and R. Wets, L-shaped linear programs with applications to optimal control and stochastic programming, SIAM Journal on Applied Mathematics 17 (1969) 638–663. https://doi.org/10.1137/0117061
• J.R. Birge and F.V. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

The price of anarchy measures how much a system of selfish agents loses compared with a centrally optimized one: it is the worst ratio, over all Nash equilibria, between the social cost of the equilibrium and the optimal social cost. Koutsoupias and Papadimitriou introduced it in 1999 (Worst-case equilibria, STACS 1999), and bounding it for routing and congestion games became a central topic of algorithmic game theory. Congestion games model routing in networks, load balancing on machines and any setting where agents choose sets of shared resources whose cost grows with their usage.

Christodoulou and Koutsoupias (The price of anarchy of finite congestion games, STOC 2005) determined the pure price of anarchy of finite (atomic, unweighted) congestion games with linear latencies for two social costs — the sum of the players' costs and the maximum cost of a player — and for asymmetric and symmetric games. Awerbuch, Azar and Epstein obtained the $5/2$ bound for the sum independently in the same proceedings (The price of routing unsplittable flow, STOC 2005). This mission is the fourth of a series that formalizes the paper: the symmetric games with the maximum social cost (Sect. 3.4). For asymmetric games the maximum social cost has price of anarchy $\Theta(\sqrt N)$ (mission III); symmetry brings it down to a constant.

Setting

A congestion game has a finite set of players $N=\{1,\dots,n\}$, a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies (each a subset of $E$), and for each facility $e$ a latency function $f_e:\mathbb N\to\mathbb R$. A pure strategy profile $A=(A_1,\dots,A_n)$ picks $A_i\in\Sigma_i$ for every player. The load $n_e(A)$ is the number of players whose strategy contains $e$, and the cost of player $i$ is

$$c_i(A)=\sum_{e\in A_i} f_e\big(n_e(A)\big).$$

A profile $A$ is a pure Nash equilibrium if no player can lower its cost by changing only its own strategy: $c_i(A)\le c_i(A_{-i},S)$ for every $i$ and every $S\in\Sigma_i$, where $(A_{-i},S)$ replaces $A_i$ by $S$.

The maximum social cost is $\mathrm{MAX}(A)=\max_{i} c_i(A)$ and the sum social cost is $\mathrm{SUM}(A)=\sum_i c_i(A)$. Latencies are linear when $f_e(k)=a_e k+b_e$ with $a_e,b_e\ge 0$. The game is symmetric when all players share one strategy set, $\Sigma_i=\Sigma$. The pure price of anarchy for the maximum social cost is

$$\mathrm{PA}=\sup_{A\ \text{Nash}}\frac{\mathrm{MAX}(A)}{\min_{P}\mathrm{MAX}(P)}.$$

Formalization targets

Goal: Theorems 7 and 8

For every symmetric linear congestion game with at least one player, every pure Nash equilibrium $A$ and every pure strategy profile $P$,

$$\mathrm{MAX}(A)\le\tfrac52\,\mathrm{MAX}(P),$$

and for every $N\ge3$ there is a symmetric linear congestion game with $N$ players, a pure Nash equilibrium $A$ and a profile $P$ that minimizes the maximum social cost, with $\mathrm{MAX}(P)>0$ and

$$\mathrm{MAX}(A)=\frac{5N+1}{2N+2}\,\mathrm{MAX}(P).$$

The second part shows that the constant $5/2$ of the first is tight as $N\to\infty$.

Milestones

1. Theorem 7, proof (first display). In a symmetric linear game, a Nash equilibrium cost is bounded by the cost of every strategy $P_j$ evaluated at loads $n_e(A)+1$: $c_i(A)\le\sum_{e\in P_j}f_e(n_e(A)+1)$.
2. Theorem 7, proof (second display). Summed over $j$: $N\cdot c_i(A)\le\sum_e n_e(P)f_e(n_e(A)+1)$.
3. Lemma 1. $\beta(\alpha+1)\le\frac13\alpha^2+\frac53\beta^2$ for nonnegative integers $\alpha,\beta$.
4. Theorem 7, proof (Lemma 1 step). $\sum_e n_e(P)f_e(n_e(A)+1)\le\frac13\mathrm{SUM}(A)+\frac53\mathrm{SUM}(P)$.
5. Theorem 1. For linear congestion games, $\mathrm{SUM}(A)\le\frac52\mathrm{SUM}(P)$ at every pure Nash equilibrium $A$.
6. Theorem 7 and Theorem 8 as separate statements.

Significance

The result says that in symmetric congestion games with linear costs no player at an equilibrium is ever more than $5/2$ times worse off than the worst-off player under the best allocation, regardless of the number of players. This contrasts with the asymmetric case, where the ratio grows like $\sqrt N$ (Theorems 5 and 6 of the paper), and it fills the symmetric–maximum entry of the paper's Table 1. Together with the sum bounds it completes the picture of pure equilibria under linear latencies that later work on smoothness and robust price of anarchy (Roughgarden, Intrinsic robustness of the price of anarchy, STOC 2009) generalized.

The results are proved in the paper, which only displays the identity-latency case and states that the arguments extend to affine latencies. No machine-checked version of any of the paper's bounds is known to exist; the mission produces a formal proof of the affine statement, a checked construction for the lower bound (the paper verifies its Nash condition only partly), and a congestion-game layer shared with the rest of the series.

Difficulty

The obvious attempt bounds the worst player's cost by its deviation to its own optimal strategy only, as in the proof for the sum; that gives one inequality per player and loses the factor $N$ needed to compare with $\mathrm{MAX}(P)$. Without symmetry the factor cannot be recovered at all (Theorem 6 of the paper). For the lower bound, the difficulty is that the construction must be a Nash equilibrium against all strategies in the common set — including the other players' equilibrium strategies and the isolated strategy of the maximum-cost player — while the paper only writes out the deviation to the optimal strategies; its parameters are left as the solution of a linear equation, which must be chosen integral for every $N\ge3$.

Formalization scope

Players form a finite type (Fin N in the lower bound) and facilities a finite type; profiles are maps from players to Finsets of facilities, with feasibility $A_i\in\Sigma_i$ as a separate predicate IsProfile. Latencies are real-valued functions on natural-number loads; "linear" means affine with nonnegative coefficients. MAX is the maximum over a nonempty player set. Upper bounds are stated for every Nash equilibrium and every feasible profile, never dividing by the optimum. The lower bound asserts that $P$ minimizes MAX over all profiles and that $\mathrm{MAX}(P)>0$: without positivity the equality would be satisfied by a game with all costs $0$, and without symmetry or the full common strategy set the instance would not be the paper's. The lower bound gives $\mathrm{PA}\ge\frac{5N+1}{2N+2}$ for the instance, which is what the paper's proof shows.

The development needs sums over facilities exchanged with sums over players ($\sum_j\sum_{e\in P_j}g(e)=\sum_e n_e(P)g(e)$), monotonicity of affine latencies, and an explicit finite instance. The congestion-game definitions are shared with the other missions of the series and will be merged with them; Lemma 1 and Theorem 1 are also milestones of mission I. Proofs of any milestone, and alternative constructions for Theorem 8, are welcome.

Selected references

• G. Christodoulou and E. Koutsoupias, The price of anarchy of finite congestion games, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar and A. Epstein, The price of routing unsplittable flow, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060599
• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563. https://doi.org/10.1007/3-540-49116-3_38
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2, 1973. https://doi.org/10.1007/BF01737559
• T. Roughgarden, Intrinsic robustness of the price of anarchy, Proc. 41st ACM STOC, 2009. https://doi.org/10.1145/1536414.1536430