Operations Research

Motivation

A linear program often has two objectives that pull in different directions, for example cost and risk, or two policy goals whose relative weight is a matter of judgment. Gass and Saaty (NRLQ 1955) put the question in its simplest form: let every cost coefficient be an affine function $d_j + \lambda d'_j$ of one real parameter $\lambda$, and find, for every value of $\lambda$, an optimal solution. Their paper turned this into a procedure that runs the simplex method once and then walks along the $\lambda$-axis, changing one basis column at a time. This parametric objective function method became a standard chapter of linear programming texts and is the prototype of parametric and sensitivity analysis in optimization software.

Timeline.

• 1951: Dantzig publishes the simplex method (Cowles Commission Monograph No. 13, Ch. XXI; the paper's reference [1]), with the optimality test $z_j - c_j \le 0$ for a minimization problem.
• 1954: Gass and Saaty summarize the parametric procedure (J. Oper. Res. Soc. Amer. 2 (1954), 316–319).
• 1955: the present paper gives the procedure in detail, proves the THEOREM that makes it work, and reports computations on the National Bureau of Standards SEAC computer.

Setting

For each real $\lambda$ the problem is

$$\text{minimize } \sum_{j=1}^n (d_j + \lambda d'_j)\,x_j \quad\text{subject to}\quad x_j \ge 0\ (j = 1,\dots,n),\qquad \sum_{j=1}^n a_{ij}x_j = a_{i0}\ (i = 1,\dots,m).$$

Write $A = (a_{ij})$, an $m\times n$ real matrix with columns $A_1,\dots,A_n$, and $b = (a_{i0})$. A basis is a list of $m$ linearly independent columns $A_{B(1)},\dots,A_{B(m)}$; its basic solution $x$ has $x_j = 0$ off the basis and $Ax = b$, and it is a basic feasible solution when also $x \ge 0$. Every column has coordinates $y_{ij}$ in the basis, $A_j = \sum_i y_{ij}A_{B(i)}$. For a cost vector $c$ the simplex method uses $z_j = \sum_i y_{ij}c_{B(i)}$; for the cost $c = d + \lambda d'$ the number $z_j - c_j$ is affine in $\lambda$:

$$z_j - c_j = \alpha_j + \lambda\beta_j .$$

The basis is optimal at $\lambda$ when $\alpha_j + \lambda\beta_j \le 0$ for all $j$ (inequalities (3)). The critical values of the basis are

$$\underline\lambda = \max_{\beta_j<0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (-\infty \text{ if all }\beta_j\ge 0),\qquad \bar\lambda = \min_{\beta_j>0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (+\infty \text{ if all }\beta_j\le 0).$$

The paper assumes throughout that the problem is nondegenerate: no basic feasible solution has more than $n - m$ zero components.

Case A is the situation where the current basis is optimal for some $\lambda$, so that (3) is consistent. If $\bar\lambda$ is finite, attained at an index $s$ with $\beta_s > 0$, and some $y_{is} > 0$, the method brings $A_s$ into the basis and removes the column $A_r$, $r = B(\ell)$, chosen by the simplex ratio test; $y_{rs} > 0$. Call the new basis $B'$ and its basic feasible solution $x'$.

Formalization targets

Goal: the THEOREM (p. 41)

$$\bar\lambda = \min\big\{\lambda\in\mathbb R : x' \text{ minimizes } (d+\lambda d')^{\top}x \text{ over } Ax = b,\ x \ge 0\big\}.$$

This contains both sentences of the paper's THEOREM: the new basis yields a minimum for at least one $\lambda$ (namely $\bar\lambda$), and the left end $\underline\lambda'$ of its interval of optimality equals $\bar\lambda$. The statement uses "least element" and so does not presuppose that the set is an interval.

Milestones

1. (3): under nondegeneracy, a basic feasible solution is a minimum at $\lambda$ if and only if $\alpha_j + \lambda\beta_j \le 0$ for all $j$.
2. (4)–(5): if (3) is consistent, it holds exactly for $\underline\lambda \le \lambda \le \bar\lambda$.
3. The reduced-cost optimality criterion and its nondegenerate converse, and feasibility of the basis after a simplex pivot (both already proved on the platform).
4. [1]: $\bar\lambda$ satisfies the inequalities (3') $\alpha'_j + \lambda\beta'_j \le 0$ of the new basis.
5. (7): $\alpha'_r = -\alpha_s/y_{rs}$ and $\beta'_r = -\beta_s/y_{rs}$.
6. (7)–(8): no $\lambda < \bar\lambda$ satisfies (3').
7. Case A stop: in the nondegenerate Case A setup, if every $y_{is} \le 0$, there is no minimum for any $\lambda > \bar\lambda$.
8. Summary (4): under the section's standing assumptions, the set of $\lambda$ for which a minimum exists is closed and connected.

Significance

The THEOREM is what makes the parametric procedure correct. The optimality intervals of successive bases meet end to end: the basis entered at $\bar\lambda$ takes over exactly where the old one stops, with no gap and no overlap. Together with the stopping rule this gives the paper's summary: starting from one optimal basis, the procedure produces a finite list of bases and characteristic values covering every $\lambda$ for which the problem has a minimum, and that set is a closed interval. The same structure underlies the piecewise linear, concave optimal value as a function of $\lambda$, the parametric right-hand-side method by duality, and the shadow-vertex simplex method.

The result is classical and its proof is short, but as printed it contains a sign slip: display (8) on p. 41 states the inequality in the wrong direction, so the contradiction the authors claim does not follow from what they wrote. The formal development states the corrected argument. To our knowledge none of these parametric statements has a machine-checked proof; the fixed-cost facts they rest on (the reduced-cost optimality criterion, Bertsimas–Tsitsiklis Theorem 3.1, and the feasibility of the pivoted basis, Theorem 3.2) are already proved on the platform in Shuze Chen's LinearOptimization library and are reused here as reference items.

Difficulty

The natural first idea is to observe that $\bar\lambda$ satisfies (3') and conclude. This proves only that the new basis is optimal at $\bar\lambda$. The statement that nothing below $\bar\lambda$ works is a statement about optimality, not about the inequalities (3'): one must know that failure of (3') at $\lambda$ means that $x'$ is not optimal at $\lambda$. That converse of the optimality test is false for a degenerate basic solution, which can be optimal while some $z_j - c_j$ is positive. The nondegeneracy assumption is therefore essential, and it must be transported to the new basic solution. The other ingredient is the pivot update of $z_j - c_j$ when one column leaves and another enters, which the paper uses through (7) without writing it down.

Formalization scope

The problem data are A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ and cost vectors d d' : Fin n → ℝ; the parameter $\lambda$ is the Lean variable t (λ is a Lean keyword). Indices are 0-based. Feasible set, optimality, bases, reduced costs, basic directions, the coordinates $y_{ij}$ (pivotColumn) and basic feasible solutions (IsSimplexState) are the published LinearOptimization definitions. The commitments and readings of the paper's phrases are:

• Sign. The platform's reduced cost is $\bar c_j = c_j - c_B'B^{-1}A_j = -(z_j - c_j)$; $\alpha_j$ and $\beta_j$ are defined as the negatives of the reduced costs for $d$ and $d'$, and (3), (3'), (5), (7) are stated in the paper's sign.
• "Yields a minimum" means that the point is feasible and its cost is at most that of every feasible point (IsLpOptimal), never a comparison of values.
• $\bar\lambda$ is finite in the THEOREM; it is the real number $-\alpha_s/\beta_s$ for an index $s$ with $\beta_s > 0$ attaining the minimum. As a function, (5) is valued in WithTop ℝ and WithBot ℝ; no real infimum of a possibly empty set is used.
• Nondegeneracy is stated for every basic feasible solution, including in the Case A stopping rule and Summary (4). The stopping rule also carries Case A consistency, and Summary (4) carries the section's available basic feasible solution. Linear independence of the rows of $A$ is assumed where the platform's criteria need it; it follows from the existence of a basis.
• "By the simplex method" is the reduced-cost optimality criterion; "the simplex prescription" is the ratio test; "no minimum" in the stopping rule is the unbounded outcome, optimal value $-\infty$, with the absence of a minimizer stated explicitly.
• The paper's interval $\delta \le \lambda \le \phi$ of interest plays no role in the THEOREM and is dropped.

The goal is not satisfied by a degenerate reading: its set is defined by optimality, not by the inequalities (3'), and its hypotheses hold on an explicit instance, so the statement is neither the definition of the critical value restated nor vacuous.

Not formalized: Case B (the search for a first $\lambda$ with a minimum), Summary (1)–(2) on the whole procedure, the no-repetition remark, the computing experience (§3) and the worked example (§4). Contributions welcome include the pivot-update formula for reduced costs, which is reusable for any simplex-based argument, and the closedness of the set of cost vectors with a finite optimum.

Selected references

• S. Gass and T. Saaty, The computational algorithm for the parametric objective function, Naval Research Logistics Quarterly 2 (1955), 39–45. https://doi.org/10.1002/nav.3800020106
• T. Saaty and S. Gass, The parametric objective function, Journal of the Operations Research Society of America 2 (1954), 316–319. https://doi.org/10.1287/opre.2.3.316
• G. B. Dantzig, Maximization of a linear function of variables subject to linear inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, Ch. XXI (Cowles Commission Monograph No. 13).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.1–3.2 and §5.2.

Motivation

A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.

Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.

Setting

Let $E$ be a finite set of states. Each state $i$ has a nonempty finite set $A(i)$ of actions, a reward $r_{ia}\in\mathbb R$ for each action, and transition probabilities $p_{iaj}\ge 0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each epoch $t=1,2,\dots$, a probability distribution on $A(X_t)$ that may depend on the whole history. A stationary policy $\pi^\infty$ uses fixed weights $\pi_{ia}$ at every epoch. A pure stationary policy $f^\infty$ always plays $f(i)\in A(i)$. Write $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$, $r(\pi)_i=\sum_a r_{ia}\pi_{ia}$, and $P(f)$, $r(f)$ in the pure case.

The average reward of $R$ from state $i$ is

$$\phi_i(R)=\liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i)\,r_{ja},$$

and $\hat\phi_i(R)$ is the same expression with $\limsup$. The AMD-value-vector is $\phi_i=\sup_R\phi_i(R)$, where $R$ ranges over all policies, and $R^*$ is average optimal if $\phi(R^*)=\phi$. A policy is Blackwell optimal if it maximises the discounted reward $v^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\mathbb E_R[r_{X_tY_t}]$ for all discount factors $\alpha$ in some interval $[\alpha_0,1)$.

For a stochastic matrix $P$, the stationary matrix $P^*$ is the Cesàro limit of $P^n$, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$. For a pure policy, $\phi(f^\infty)=P^*(f)r(f)$ and $u(f^\infty)=D(f)r(f)$.

A vector $\tilde\phi$ is AMD-superharmonic if some $\tilde u$ satisfies $\tilde\phi_i\ge\sum_jp_{iaj}\tilde\phi_j$ and $\tilde\phi_i+\tilde u_i\ge r_{ia}+\sum_jp_{iaj}\tilde u_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ with $\sum_j\beta_j=1$, the primal program (4.2.10) minimises $\sum_j\beta_j\tilde\phi_j$ over such pairs. Its dual is

$$\max\Big\{\sum_{i,a}r_{ia}x_{ia}\ \Big|\ \sum_{i,a}(\delta_{ij}-p_{iaj})x_{ia}=0,\ \ \sum_ax_{ja}+\sum_{i,a}(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\ \ (j\in E),\ \ x,y\ge0\Big\}.\tag{4.2.11}$$

Write $E_x=\{i\mid\sum_ax_{ia}>0\}$.

Formalization targets

Goal: Theorem 4.2.4

If $(x^*,y^*)$ is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule $f_*$ with

$$x^*_{if_*(i)}>0\ \ (i\in E_{x^*}),\qquad y^*_{if_*(i)}>0\ \ (i\in E\setminus E_{x^*})$$

exists, and every such $f_*^\infty$ is average optimal.

The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming $f_*$.

Milestones

1. Optimality equations (Theorem 4.2.1): a Blackwell optimal pure policy gives $(\phi^\circ,u^\circ)$ with $\phi^\circ_i=\max_{a\in A(i)}\sum_jp_{iaj}\phi^\circ_j$ and $\phi^\circ_i+u^\circ_i=\max_{a\in\bar A(i)}\{r_{ia}+\sum_jp_{iaj}u^\circ_j\}$.
2. Superharmonic characterisation (Theorem 4.2.2): $\phi$ is the smallest AMD-superharmonic vector.
3. Lim sup optimality (Theorem 4.2.3): a pure stationary average optimal $f^\infty$ satisfies $\hat\phi(f^\infty)\ge\hat\phi(R)$ for every $R$.
4. The three propositions inside the proof of Theorem 4.2.4: complementary slackness along $f_*$ (4.2.1), closedness of $E_{x^*}$ under $P(f_*)$ (4.2.2), and transience of $E\setminus E_{x^*}$ under $P(f_*)$ (4.2.3).
5. The policy–solution correspondence (§4.3): the representative $(x(\pi),y(\pi))$ is feasible (Theorem 4.3.1); the map is one-to-one with inverse (4.3.1) (Theorem 4.3.2); $E_x$ is closed under, and is exactly the recurrent set of, $P(\pi(x,y))$ (Propositions 4.3.2–4.3.3); the correspondence preserves optimality (Theorem 4.3.3); pure policies map to extreme points (Theorem 4.3.4).
6. Policy evaluation (Theorem 4.4.1): the system $(I-P(f))\tilde\phi=0$, $\tilde\phi+(I-P(f))\tilde u=r(f)$, $\tilde u+(I-P(f))\tilde z=0$ is solvable, and every solution has $\tilde\phi=\phi(f^\infty)$ and $\tilde u=u(f^\infty)$.

Significance

Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.

The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.

Difficulty

Under a unichain assumption, the dual variables $x$ form a stationary distribution and the $y$-variables are unnecessary, so the obvious argument reads a policy off $x$ alone. In the multichain case the $x$-part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off $y$. The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of $\phi(f_*^\infty)$ with $\phi$ must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, $\phi_i(R^*)=\sup_R\phi_i(R)$ for every $i$. It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from $i$ leads back to $i$. The ergodic set of a recurrent state is the set of states accessible from it.

A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights $\beta_j$ are strictly positive and sum to one, as in (4.2.10).

The proofs need finite Markov chain theory: the Cesàro limit, $P^*P=PP^*=P^*$, $P^*D=0$, transience versus $P^*_{\cdot j}=0$, and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• E. V. Denardo and B. L. Fox, Multichain Markov renewal programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Motivation

A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.

Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.

Timeline, following the paper's introduction:

• 1960: d'Epenoux introduces linear programming for the discounted case; De Ghellinck and Manne treat the unichain average case.
• 1962: Blackwell (DOI 10.1214/aoms/1177704593) proves that some pure stationary policy is discounted-optimal for all discount factors near 1, and expands the discounted value near $\alpha = 1$.
• 1968–1970: Denardo and Fox (DOI 10.1137/0116038) and Denardo (DOI 10.1287/mnsc.16.5.281) give the first analysis of linear programs for the multichain case. Derman's 1970 monograph streamlines it: in the worst case two linear programs and one search problem must be solved. Denardo and Fox record Bruce Miller's conjecture that the policy of Theorem 7 below is optimal.
• 1979: Hordijk and Kallenberg prove the conjecture (Theorem 7), so one linear program suffices.

Setting

The state space is a finite nonempty set $E$. In state $i$ a finite nonempty set $A(i)$ of actions is available; choosing $a \in A(i)$ earns the reward $r_{ia}$ and moves the system to state $j$ with probability $p_{iaj}$ ($p_{iaj} \ge 0$, $\sum_j p_{iaj} = 1$). A policy $R$ chooses actions at times $t = 1, 2, \dots$, possibly at random and using the whole history. For a policy $R$ and an initial state $i$,

$$\varphi_i(R) = \liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a \mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$$

is the average expected reward, and $\varphi_i = \sup_R \varphi_i(R)$ is the optimal one. A policy $R^*$ is average optimal if $\varphi_i(R^*) = \varphi_i$ for every $i \in E$. A decision rule $f$ picks $f(i) \in A(i)$ in every state; $f^\infty$ is the pure stationary policy that always applies $f$. Its transition matrix is $P(f) = (p_{if(i)j})$ and its reward vector $r(f) = (r_{if(i)})$. The α-discounted value $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\sum_j\sum_a\mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$ enters through Theorems 1, 3, 4 and 5.

Fix weights $\beta_j > 0$ with $\sum_j \beta_j = 1$. The dual program has a variable pair $x_{ia}, y_{ia}$ for every state $i$ and every $a \in A(i)$:

$$\max \sum_i\sum_a r_{ia}x_{ia}\quad\text{s.t.}\quad \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\quad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j,\quad x,y\ge0,$$

for all $j \in E$. Its linear programming dual, the primal program, minimizes $\sum_j\beta_j\tilde\varphi_j$ over superharmonic pairs $(\tilde\varphi,\tilde u)$: $\tilde\varphi_i \ge \sum_j p_{iaj}\tilde\varphi_j$ and $\tilde\varphi_i + \tilde u_i \ge r_{ia} + \sum_j p_{iaj}\tilde u_j$ for all $a \in A(i)$, $i \in E$. For a dual solution $(x, y)$ put $E_x = \{i \mid \sum_a x_{ia} > 0\}$.

Formalization targets

Goal: Theorem 7

Let $(x, y)$ be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let $f$ be any decision rule with

$$x_{if(i)} > 0 \ \ (i \in E_x), \qquad y_{if(i)} > 0 \ \ (i \notin E_x).$$

Then $f^\infty$ is average optimal: $\varphi_i(f^\infty) = \varphi_i$ for every $i \in E$, the comparison running over all policies.

Milestones

In the order the proof uses them:

1. Theorem 1 (Blackwell): some pure stationary $f_0^\infty$ is α-discounted optimal for all α near 1.
2. Theorem 2a: $\varphi(f^\infty) = P^*(f)r(f)$. The other clauses of Theorem 2 are Blackwell's Lemma 1(a), (d), referenced as published theorems.
3. Theorem 3 (Blackwell): $v_i^\alpha(f^\infty) - \varphi_i(f^\infty)/(1-\alpha) \to (D(f)r(f))_i$ as $\alpha \uparrow 1$.
4. Theorem 4 (Derman): the policy of Theorem 1 is average optimal.
5. Theorem 5: $\varphi^0 = \varphi(f_0^\infty)$ and $u^0 = D(f_0)r(f_0)$ solve the two nested optimality equations.
6. Proof of Theorem 6: $(\varphi^0, u^0 + M\varphi^0)$ is superharmonic for some $M$.
7. Theorem 6: $\varphi$ is the smallest function that admits $u$ with $(\varphi, u)$ superharmonic.
8. §3.2: $(\varphi(f_0^\infty), D(f_0)r(f_0) + M\varphi(f_0^\infty))$ is primal optimal for all large $M$.
9. Proof of Theorem 7: $\sum_a x_{ja} + \sum_a y_{ja} \ge \beta_j > 0$, so the rule always defines a policy; and every primal optimum has first component $\varphi$.
10. Propositions 1–3: $\varphi$ is $P(f)$-harmonic and the gain–bias equation holds on $E_x$; $E_x$ is closed under $P(f)$; at an extreme optimal dual solution, the states outside $E_x$ are transient under $P(f)$.

Significance

Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive $x$-variable, otherwise any action with a positive $y$-variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.

The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.

Difficulty

The obvious argument reads $f$ off any optimal dual solution and uses complementary slackness to obtain $\varphi = P(f)\varphi$ and $\varphi + (I - P(f))u = r(f)$. The second equation holds only on $E_x$, and outside $E_x$ nothing controls the reward of $f$. The argument closes only when $E \setminus E_x$ is transient under $P(f)$, so that the stationary distribution of $f$ ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside $E\setminus E_x$ would make the corresponding $y$-columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from $(x, y)$ (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.

Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near $\alpha = 1$. Both compare against all history-dependent policies and need the full limit theory of $P^*$ and $D$.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. $\varphi_i(R)$ is gainInf (the lim inf of the average of the first $T$ expected rewards) and $\varphi_i$ is optGainInf, a real supremum that is finite because rewards are bounded. $P^*$ and $D$ are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:

• Average optimality is Hordijk and Kallenberg's $\varphi(R^*) = \varphi$, not the stronger Puterman criterion IsAverageOptimal in the published file.
• The discounted value is the limit of the $N$-epoch discounted reward, defined by the same backward recursion as totalReward. "α near enough to 1" means some $\alpha_0 \in [0,1)$ such that the property holds on $[\alpha_0, 1)$.
• Dual variables are indexed by the admissible pairs only (Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.
• "The simplex method is used" is encoded as "$(x, y)$ is an extreme point of the feasible set" (Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some $f$ instead of every $f$ obeying the rule is weaker than the paper's. Both are ruled out.
• "Transient" is the negation of the published IsRecurrent. Maxima over $A(i)$ and $A^0(i)$ are stated as an upper bound plus attainment, so that $A^0(i) \ne \emptyset$ is part of Theorem 5.

A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of $\{z \ge 0 : Az = b\}$ by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with $P^*r$. Contributions to any of them, including proofs of individual milestones, are welcome.

Selected references

• A. Hordijk, L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
• E. V. Denardo, B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
• J. G. Kemeny, J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• C. Derman, Finite State Markovian Decision Processes, Academic Press, 1970.

Motivation

Value iteration computes the optimal value function of a Markov decision process by applying the dynamic programming backup to every state until the values stop changing. When the state space is too large for a lookup table, practitioners replace the table by a function approximator: after each backup, the new values are computed only at a sample of states and an approximator (a neural net, a spline, a nearest-neighbour rule) is fitted to them. This approximate value iteration is the basis of much of reinforcement learning, and in the early 1990s it was known to work well in some experiments and to diverge in others, with no theory separating the two. Boyan and Moore (NIPS 7, 1995) exhibited divergence with linear regression and neural nets, and Tsitsiklis and Van Roy (1996) later studied the same question for feature-based architectures.

Gordon's technical report (CMU-CS-95-103, 1995; a shorter, differently numbered version appeared at ICML 1995) isolated a property of the approximator that guarantees convergence: the approximator must not exaggerate differences between target value functions in max norm. It identified a broad class with this property, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a mesh), and proved that in a discounted problem approximate value iteration through an averager always converges, with an explicit error bound. This mission formalizes that discounted theory: the report's §2–§3 and its error bound of §6.1.

Setting

A finite Markov decision process $M$ has states $1,\dots,n$, a finite nonempty set $U(i)$ of actions at each state $i$, an expected one-step cost $c_{ia}$ for action $a$ at state $i$, and transition probabilities $p_{aij}\ge0$ with $\sum_j p_{aij}=1$. It is discounted with factor $0\le\gamma<1$. A value function is a vector $V\in\mathbb R^n$, measured in the max norm $\|V\|=\max_i|V(i)|$.

The parallel value backup operator $T_M$ updates every state at once:

$$(T_MV)(i)=\min_{a\in U(i)}\Big(c_{ia}+\gamma\sum_{j=1}^n p_{aij}V(j)\Big).$$

Its fixed point $V^*$ is the optimal value function, the minimal expected discounted cost from each state.

A function approximator is studied through its mapping $M_F$: the function sending a vector of target values to the vector of fitted values. Two operators $M_F$ and $T$ are compatible if the iterates $(M_F\circ T)^k(x_0)$ converge from every initial guess $x_0$.

An averager $A$ is given by constants $k_i$ and nonnegative weights $\beta_i,\beta_{ij}$ with $\beta_i+\sum_j\beta_{ij}=1$ for every $i$; its mapping is

$$M_A(Y)_i=\beta_ik_i+\sum_{j=1}^n\beta_{ij}Y_j .$$

The weights are fixed in advance and do not depend on the targets $Y$.

Formalization targets

Goal: Theorem 6.2 (p. 12)

Let $V^A$ be any fixed point of $M_A$ and $\varepsilon=\|V^A-V^*\|$. Then there is $V_0$ such that $(T_M\circ M_A)^k(V)\to V_0$ from every initial guess $V$, and

$$\|V_0-V^*\|\le\frac{2\gamma\varepsilon}{1-\gamma}.$$

The goal has two parts: convergence from every start to a common limit $V_0$, and the error bound on that limit.

Milestones

1. Theorem 2.2, first clause (p. 4). $\|T_MV-T_MW\|\le\gamma\|V-W\|$.
2. Theorem 3.2 (p. 7). $M_A$ is a max-norm nonexpansion, $\|M_A(Y)-M_A(Z)\|\le\|Y-Z\|$, and is compatible with $T_M$ for every discounted MDP.
3. Theorem 3.1 (p. 5). If $M_F$ is any max-norm nonexpansion, then $M_F$ is compatible with $T_M$ and $\|M_F(T_MV)-M_F(T_MW)\|\le\gamma\|V-W\|$.
4. Corollary 3.1 (p. 6). There is $V_\infty$ with $\|(M_F\circ T_M)^k(V)-V_\infty\|\le\gamma^k\|V-V_\infty\|$ for all $V$ and $k$.

A further item, not a milestone, is the display after the proof of Theorem 6.2 (p. 13), the bound on the fitted output: $\|V^*-M_A(V_0)\|\le2\varepsilon+2\gamma\varepsilon/(1-\gamma)$.

Significance

Theorem 6.2 gives a guarantee that depends only on how well the approximator can represent $V^*$, not on how the iteration is started: if some fixed point of the averager lies within $\varepsilon$ of $V^*$, approximate value iteration finds a function within $2\gamma\varepsilon/(1-\gamma)$ of $V^*$. Theorems 3.1 and 3.2 explain why: an averager is a max-norm nonexpansion, and composing a nonexpansion with a $\gamma$-contraction leaves a $\gamma$-contraction. Together they separate the approximators that are safe to use with value iteration from those that are not (linear regression is not a nonexpansion: the report's Figure 2 shows it can expand max-norm distances).

All results of this mission are proved in the report; none is open. The contraction of the discounted Bellman operator and the identification of its fixed point with the optimal value function are proved on Prove2Me (BertsekasDP.discounted_main_theorem, used here as a reference item). No machine-checked proof of Gordon's averager results or of the $2\gamma\varepsilon/(1-\gamma)$ bound is known to exist; this mission produces one, on top of the published finite MDP model.

Difficulty

Each step is short on paper; the difficulty is in the bookkeeping that a formal proof cannot skip. The nonexpansion of an averager rests on nonnegative weights summing to at most one, which must be extracted from the row constraint $\beta_i+\sum_j\beta_{ij}=1$ in the max norm on $\mathbb R^n$. The goal's convergence clause asks for one limit $V_0$ shared by all initial guesses, which needs completeness of $\mathbb R^n$ and the contraction-mapping theorem applied to $T_M\circ M_A$, not to $T_M$. The error bound compares three different fixed points ($V^*$ of $T_M$, $V^A$ of $M_A$, $V_0$ of $T_M\circ M_A$) in a chain of triangle inequalities. The order of composition matters throughout: the compatibility results iterate $M_F\circ T_M$ (fit after the backup), while the goal iterates $T_M\circ M_A$ (back up after the fit), and the two may not be interchanged.

Formalization scope

• The MDP is the published BertsekasSSPModel (Fin n states, a finite action type, nonempty admissible action sets $U(i)$, costs g, transition probabilities p), and $T_M$ is its BertsekasDiscountedBellmanOp M γ. That model allows substochastic rows; every statement adds the hypothesis $\sum_j p_{aij}=1$ for admissible $a$, which makes it the report's MDP. Action sets may depend on the state, a harmless generalization of the report's single action set. The initial-state distribution $S_0$ never enters a statement and is omitted.
• The discount satisfies $0\le\gamma<1$ in every item. Theorem 6.2's page says only "with discount factor $\gamma$"; it belongs to the report's discounted discussion and its proof uses that $T_M$ is a $\gamma$-contraction.
• $\|\cdot\|$ on Fin n → ℝ is Mathlib's sup norm, i.e. the max norm.
• $V^*$ is a hypothesis: a fixed point of $T_M$. Theorem 2.2's last clause, proved on the platform as BertsekasDP.discounted_main_theorem, identifies it with the optimal value function.
• The averager acts on whole value functions $\mathbb R^n\to\mathbb R^n$, indexed by the states. The report's approximator fits a sample $X_0$ of states; ignoring the value at a state $j$ outside the sample is the special case $\beta_{ij}=0$.
• Theorem 3.1 is printed with "$X=S\times A$" and $M_F\in\mathbb R^{|X|}\mapsto\mathbb R^{|X|}$; since $T_M$ acts on value functions of the state, $M_F$ is stated on $\mathbb R^n$.
• "Converges at the rate $\gamma$" (Corollary 3.1) is the geometric rate of the contraction-mapping theorem, $\gamma^k$ times the initial distance to the limit.
• Theorem 6.2 keeps $\varepsilon=\|V^A-V^*\|$ as an equality, as printed, and its conclusion keeps the convergence clause. A statement asserting only the existence of some $V_0$ with $\|V_0-V^*\|\le2\gamma\varepsilon/(1-\gamma)$ would be trivial ($V_0=V^*$) and is not the theorem.
• Lemma 2.1 and the Contraction Mapping theorem (Theorem 2.1) are in Mathlib (LipschitzWith.comp, ContractingWith) and are not posed.

Proofs of any item are welcome, as are reusable lemmas on max-norm nonexpansions of row-stochastic linear maps, which also serve the nondiscounted companion mission (Stable Function Approximation in Dynamic Programming II).

Selected references

• G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995; shorter version in Machine Learning Proceedings 1995 (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989 (the report's [BT89]; no DOI).
• J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, MIT Press, 1995 (the report's [BM95]).
• J. N. Tsitsiklis and B. Van Roy, Feature-Based Methods for Large Scale Dynamic Programming, Machine Learning 22, 1996, pp. 59–94. https://doi.org/10.1007/BF00114724

Motivation

The Chinese postman problem, posed by Meigu Guan (Kwan Mei-Ko) in 1962, asks for a shortest closed walk in a graph that traverses every edge at least once: the route of a postman who must cover every street and return to the post office. It is the basic model of arc routing (street sweeping, snow ploughing, meter reading, inspection of networks), and it is one of the first combinatorial optimization problems shown to be solvable in polynomial time by matching methods.

Edmonds and Johnson, Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), reduce the postman problem to a parity problem: choose nonnegative integers $x_e$, the number of extra traversals of each edge, so that every node becomes even, at minimum total length. Their §3 gives a complete linear description of this parity problem. The description is the first instance of what is now called the $T$-join polyhedron (with $T$ the set of odd-degree nodes), a standard object of polyhedral combinatorics and a frequent example of total dual integrality.

Timeline:

• 1962: Guan states the postman problem and an optimality criterion for it.
• 1965: Edmonds proves the matching polyhedron theorem and gives the blossom algorithm for weighted matching (Edmonds 1965).
• 1973: Edmonds and Johnson specialise both to the postman problem, giving the polyhedron in the edge variables alone (this mission) and a blossom algorithm that solves it (Edmonds–Johnson 1973).

Setting

A graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges; each edge meets two different nodes, and several edges may meet the same pair of nodes. The degree of a node $n$ is the number of edges meeting it, $\sum_{e\in E} a_{ne}$, where $a_{ne}=1$ if $e$ meets $n$ and $0$ otherwise. Set $b_n=1$ when the degree of $n$ is odd (an odd node) and $b_n=0$ otherwise.

An edge $e$ meets a set $S\subseteq N$ when exactly one of its two ends lies in $S$. A set $S\subseteq N$ is an odd set when it contains an odd number of odd nodes, and any number of even nodes.

The parity points $X\subseteq\mathbb R^E$ are the vectors with

$$x_e\in\mathbb Z,\quad x_e\ge 0\quad(e\in E),\qquad \sum_{e\in E}a_{ne}x_e\equiv b_n \pmod 2\quad(n\in N),$$

the conditions (3.1), (3.2), (3.6) of the paper. Adding $x_e$ copies of each edge $e$ to $G$ makes every degree even, and an Euler tour of the enlarged graph is a postman tour of $G$. The postman polyhedron is

$$P=\Big\{x\in\mathbb R^E:\ x_e\ge 0\ (e\in E),\ \ \sum\{x_e : e\text{ meets }S\}\ge 1\ \text{for every odd set } S\Big\},$$

the conditions (3.2) and (3.5). For lengths $c\in\mathbb R^E$ the objective is $z=\sum_e c_e x_e$. The dual linear program has a variable $y_S$ for each odd set, constraints $y_S\ge 0$ and $\sum\{y_S: e\text{ meets }S\}\le c_e$, and objective $v=\sum_S y_S$.

Formalization targets

Goal: the polyhedron theorem (p. 93)

$$\operatorname{conv} X = P .$$

Both inclusions are claimed. The equality is between subsets of $\mathbb R^E$, so it also asserts that the convex hull of $X$ is closed.

Milestones

In the paper's order of argument:

1. (3.13), p. 95: an integer solution of (3.6) has $\sum\{x_e : e\text{ meets }S\}\equiv 1 \pmod 2$ for every odd set $S$.
2. p. 95: $\operatorname{conv}X\subseteq P$.
3. (3.10), p. 94: weak duality, $v\le z$ for $x\in P$ and $y$ dual feasible.
4. (3.11)–(3.12), p. 95: complementary slackness makes $x$ and $y$ optimal.
5. p. 95: for $c\ge 0$ there is an integral parity point $x$ and a dual feasible $y$ satisfying (3.11) and (3.12). The paper proves this with the algorithm of §4.
6. p. 96: if some $c_e<0$, $z$ is unbounded below on $P$ and on $X$.
7. (3.19), p. 96: for $c\ge 0$, the minimum of $z$ over $P$ is attained at a parity point.

There are two companion statements. The first (pp. 93–94) says that in $\sum_e a_{ne}x_e-2w_n=b_n$ with $x\ge 0$, integrality of $w_n$ already forces $w_n\ge 0$. The second (p. 91) is the polyhedron theorem in the variables $(x,w)$: the convex hull of the integer solutions of (3.1)–(3.3) is the set of solutions of (3.2), (3.2′), (3.3), (3.5).

Significance

The theorem turns the parity problem, an integer program, into a linear program over an explicitly described polyhedron. Optimal postman tours therefore come with dual certificates: a packing of odd cuts whose total value matches the tour's extra length. The same description underlies the theory of $T$-joins and $T$-cuts (Schrijver 2003, Chapter 29).

No machine-checked proof of the $T$-join polyhedron theorem exists, on Prove2Me or, to our knowledge, in Mathlib. This mission states it in the multigraph setting of the paper. Milestones 1–4 and 6 are elementary and can serve as warm-ups. Milestone 5, total dual integrality of the odd-cut system, is the substantive step. The paper obtains it from a blossom algorithm; the milestone is stated as an existence result, so any proof of it closes it.

Difficulty

The inclusion $\operatorname{conv}X\subseteq P$ is a parity count. The reverse inclusion is the theorem. Two first ideas fail. Total unimodularity does not apply, because the odd-cut constraint matrix is not totally unimodular and $P$ has many constraints whose tightness interacts. Reading the result off the matching polyhedron theorem needs the auxiliary loops $w_n$ and an elimination step, and the 1965 matching polyhedron describes perfect matchings of a simple graph, not this parity system on a multigraph. Some argument for integrality of the minimum for every $c\ge 0$ is needed, and the paper's is an algorithm with a dual certificate. A further point is that $P$ and $X$ are unbounded: equality of hulls is not just agreement of minima over bounded objectives, and the case of objectives with a negative coefficient has to be handled separately (milestone 6).

Formalization scope

A graph is the local ChinesePostman.Polyhedron.Graph V E: a map ends : E → Sym2 V with a proof that no edge is a loop, over finite types V and E. Mathlib's SimpleGraph is not used, because the paper allows parallel edges. Degrees, odd nodes and $b_n$ are computed from the graph; the set of odd nodes is never a free parameter. "$e$ meets $S$" means exactly one end in $S$. Odd sets range over all subsets $S\subseteq N$ with an odd number of odd nodes, with no nonemptiness or properness condition. Parity points are real images of integer vectors E → ℤ, so integrality is part of $X$. Dual variables are functions Finset V → ℝ whose values matter only on odd sets: the sign condition and every sum are restricted to the odd sets. Lengths $c$ are arbitrary reals except where the page assumes $c_e\ge 0$ (milestones 5 and 7).

Trivializing readings are ruled out: (3.5) taken over nonempty proper sets only, "meets" read as "has at least one end in", the odd nodes taken as an arbitrary set $T$, or $X$ allowed to contain non-integral points would each give a different, and in some cases false or trivial, statement.

Every definition the statements need is in one file, ChinesePostman.Polyhedron.Setting. A complete development needs finite-dimensional convexity (Mathlib's convexHull) and linear programming duality or an integrality argument. A Lean proof of total dual integrality for odd-cut systems would be reusable for matching and $T$-join problems beyond this paper. Proofs of any milestone, and alternative proofs of milestone 5, are welcome.

Selected references

• J. Edmonds and E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• M. Guan (Kwan Mei-Ko), Graphic programming using odd or even points, Chinese Mathematics 1 (1962) 273–277.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 29 (T-joins and T-cuts). https://doi.org/10.1007/978-3-540-44389-6

Motivation

Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.

The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector $Q$, Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.

Setting

A depot $P_0$ serves customers $P_1,\dots,P_M$. The distance $d_{y,z}$ between every two points is given, and customer $P_j$ requires a load $q_j$. Trucks come in $n$ capacity classes: $x_i$ trucks of capacity $C_i$ are available, with $C_1<\dots<C_n$, and the trucks of the smallest capacity are unlimited, $x_1=\infty$ (p. 569).

A run is the ordered list of customers $P_{a_1},\dots,P_{a_k}$ served by one truck, which drives $P_0P_{a_1}\cdots P_{a_k}P_0$. Its load is $\sum_i q_{a_i}$. A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.

The saving of the cell $(y:z)$ is $d_{0,y}+d_{0,z}-d_{y,z}$. The half matrix records $t_{y,z}=1$ if $P_y$ and $P_z$ are adjacent on a run, and $t_{y,0}\in\{0,1,2\}$ counts how many ends of runs lie at $P_y$. Table II counts, for each capacity level $C_i$, the runs with load above $C_i$ and the trucks with capacity above $C_i$.

The procedure starts with the runs $[P_1],\dots,[P_M]$, so $t_{y,0}=2$ for every customer. A cell $(y:z)$ is admissible if (I) $t_{y,0}>0$ and $t_{z,0}>0$; (II) $P_y$ and $P_z$ are on different runs; (III) after replacing those two runs by one run of load $Q_y+Q_z$, no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at $P_y$ and $P_z$. The procedure stops when no cell is admissible.

Formalization targets

Goal: correctness of the procedure

Assume symmetric distances, $C_1<\dots<C_n$, $x_1=\infty$, and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state $S$ is a feasible allocation satisfying relation (A), $\sum_{z\ne y}t_{y,z}=2$ for every customer, with

$$\text{mileage}(S)=2\sum_{j=1}^M d_{0,j}-\sum_{\substack{1\le y<z\le M\\ t_{y,z}=1}}\bigl(d_{0,y}+d_{0,z}-d_{y,z}\bigr).$$

Milestones

$$\text{mileage}(\text{link}(S,y,z))=\text{mileage}(S)-(d_{0,y}+d_{0,z}-d_{y,z})\quad\text{for admissible }(y:z),$$

relation (A) at every reachable state, the permanence of links between customers, and

$$\#\{\text{runs with load}>C_i\}\le\sum_{k>i}x_k\ \ (i=1,\dots,n)\iff\text{the runs can be allocated to trucks},$$

which together give feasibility of every reachable state. Two further milestones: when $C_n\ge\sum_j q_j$ and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.

Significance

The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.

None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.

Difficulty

The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both $x_1=\infty$ and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.

Formalization scope

Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's $C_{i+1}$; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix $t$ and the vector $Q$ are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.

Choices committed to:

• distances are arbitrary real, symmetric numbers (the half matrix, p. 573); no nonnegativity or triangle inequality is assumed in the goal, and savings may be negative;
• every run: ties are free, as the paper suggests choosing randomly;
• reachable states: invariants are not claimed for arbitrary lists of runs;
• Table II is read cumulatively: column "Over $C_i$" compares runs with load $>C_i$ against all trucks of capacity $>C_i$, as the printed Tables II, IV and VI show;
• $x_1=\infty$ and $C_1<\dots<C_n$ are hypotheses; $q_j\le C_n$ is not separately assumed, since it follows from the initial Table II test;
• the initial one-truck-per-customer allocation is assumed feasible (p. 572);
• the metric hypotheses enter only the traveling-salesman milestone.

A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.

Not formalized: the informal $C_1\ll\sum q_j$, the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.

Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.

Selected references

• G. Clarke and J. W. Wright, Scheduling of vehicles from a central depot to a number of delivery points, Operations Research 12(4) (1964), 568–581. https://doi.org/10.1287/opre.12.4.568
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6(1) (1959), 80–91. https://doi.org/10.1287/mnsc.6.1.80
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26

Motivation

Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.

The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching $1-1/e$ of the $n$ pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.

Setting

A bipartite graph has a boy side $U$ and a girl side $V$, each with $n$ vertices. An edge $(u,v)$ means that boy $u$ may be paired with girl $v$. A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.

Girls arrive in a predetermined order. When girl $v$ arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation $\pi$ of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write $M_{\mathrm R}(G,\pi)$ for the final matching. The expected size is the finite average over all $n!$ rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to $n,n-1,\ldots,1$.

The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered $1,\ldots,n$ and column $n$ has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge $(i,i)$ and with an edge $(i,j)$ only when $i\le j$. On such a graph, the auxiliary algorithm EARLY declines to match row $i$ if column $i$ is already covered by EARLY's own matching. For any matching $M$, $D(M)$ denotes the indices for which both row $i$ and column $i$ are covered.

Formalization targets

RANKING guarantee

For every $\varepsilon>0$, one threshold $N$ must work for every size $n\ge N$ and every graph $G$ with a perfect matching:

$$\mathbb E_{\pi\sim\mathrm{Unif}(S_n)}|M_{\mathrm R}(G,\pi)| \ge (1-e^{-1}-\varepsilon)n.$$

This is the uniform lower-bound reading of the paper's $n(1-1/e)-o(n)$ target. It does not prescribe a finite-$n$ additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.

Significance

The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic $1-1/e$ fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.

A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.

Difficulty

The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.

Formalization scope

Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column $n-1$ as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.

All expectations are finite averages over Equiv.Perm (Fin n), scaled by $1/n!$. The formal $o(n)$ claim is $\forall\varepsilon>0,\ \exists N,\ \forall n\ge N,\ \forall G$ with a perfect matching, the displayed lower bound. Placing $N$ before $G$ preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.

The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.

Selected references

• Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, 1990, pp. 352–358. DOI: 10.1145/100216.100262.

Why competing retailers change the contracting problem

A supplier who sells through a single newsvendor retailer faces double marginalization: the retailer bears the whole cost of leftover stock but earns only the retail margin, so under a plain wholesale-price contract he orders less than the integrated supply chain would. The literature reviewed in G. P. Cachon's chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) shows that buy-back, revenue-sharing and related contracts correct this distortion. Section 6.5 asks what happens when the supplier sells through several retailers who compete for the same customers.

Competition can push in the opposite direction. When customers buy wherever stock is available, a retailer who stocks more also takes demand from his rivals, and he does not count that loss as a cost. This demand-stealing effect pushes the retailers towards over-ordering, which offsets double marginalization. §6.5.1 makes this precise in the proportional allocation model, in which total demand is split among the retailers in proportion to their inventories. The model goes back to the deterministic version of Wang and Gerchak (2001); related allocation models are those of Lippman and McCardle (1997) and Anupindi and Bassok (1999), and Mahajan and van Ryzin (2001) observe the same mitigation of the need for coordinating contracts.

This mission formalizes §6.5.1 of the chapter's January 2003 third draft, pp. 48–53.

The proportional allocation model

There are $n \ge 2$ retailers and one supplier. Total retail demand $D \ge 0$ is random, with distribution function $F$ that is differentiable on $(0,\infty)$ with density $f$, strictly increasing on $[0,\infty)$, and satisfies $F(0)=0$. The retail price is $p$ and the supplier's unit production cost is $c$, with $0 < c < p$. Goodwill costs, the salvage value and the retailers' handling cost are zero.

Retailer $i$ orders $q_i \ge 0$. Write $q = \sum_j q_j$ and $q_{-i} = q - q_i$. Retailer $i$ receives the demand $D_i = (q_i/q)D$. Under a buy-back contract $(w, b)$ he pays $w$ per unit ordered and is refunded $b$ per unit left over; $b = 0$ is the wholesale-price contract. His expected profit is

$$\pi_i(q_i, q_{-i}) = \mathbb E\big[p\min(q_i, D_i) + b(q_i - D_i)^+\big] - wq_i = (p-w)q_i - (p-b)\frac{q_i}{q}\int_0^q F(x)\,dx .$$

Because total sales $\min(q, D)$ depend only on the total stock, the integrated chain earns $\Pi(q) = pS(q) - cq$ with $S(q) = \mathbb E[\min(q,D)]$, and its optimal stock $q^o$ solves the newsvendor equation $F(q^o) = (p-c)/p$, Eq. (20). A Nash equilibrium is a profile of orders in which each $q^*_i$ maximizes $\pi_i(\cdot, q^*_{-i})$ over all orders $x \ge 0$. A contract coordinates the chain when its equilibrium total order is $q^o$.

Two contract prices appear on p. 52: the wholesale price $\widehat w(q) = p\big(1 - \tfrac1n F(q) - \tfrac{n-1}{n}\cdot\tfrac1q\int_0^qF\big)$ that induces total stock $q$, and the buy-back wholesale price

$$w_b(b) = p - (p-b)\left[\frac1n\cdot\frac{p-c}{p} + \frac{n-1}{n}\cdot\frac{1}{q^o}\int_0^{q^o}F(x)\,dx\right].$$

Formalization targets

Goal: the coordinating buy-back contract (pp. 51–53)

For $n \ge 2$, $b < p$ and $q^o$ solving (20), with $w = w_b(b)$: $q^o$ maximizes $\Pi$; $b < w_b(b) < p$; the profile in which every retailer orders $q^o/n$ is the unique Nash equilibrium; and at that equilibrium

$$\pi_i = \frac{p-b}{pn^2}\,\Pi(q^o), \qquad \pi_s = wq^o - cq^o - b\,\mathbb E[(q^o-D)^+] = \frac{p(n-1)+b}{pn}\,\Pi(q^o).$$

Milestones

The milestones are the section's own claims, in attack order: the newsvendor characterization (20); the inequality $\frac1q\int_0^qF < F(q)$; the closed form of $\pi_i$ and its strict concavity in the retailer's own order (p. 50); the first-order condition and Eq. (21); the monotonicity and limits of the left side $L_n$ of Eq. (22), giving a unique root for $b < w < p$; the unique, symmetric Nash equilibrium for every $b < w < p$; the increase of the equilibrium total in $n$; that $\widehat w(q)$ induces $q$, that $\widehat w(q^o) > c$, and that the supplier's profit under wholesale pricing has negative slope at $q^o$; the coordinating price $w_b(b)$ with $w_b(b) > \widehat w(q^o)$ for $b > 0$; and the ratio $\pi_s(q^o, w_b(0), 0)/\Pi(q^o) = (n-1)/n$ (p. 53). A companion item states the endpoint $b = p$, at which the supplier takes all of $\Pi(q^o)$.

Significance

The section answers two questions. First, with competing retailers a plain wholesale-price contract can coordinate the chain and still leave the supplier a positive margin, which a single retailer never allows. Second, that contract is not the supplier's best wholesale price, and it fixes a single division of profit. Buy-back contracts remove both limitations: the family $(w_b(b), b)$ coordinates for every $b < p$ and moves the supplier's share continuously from $(n-1)/n$ to all of $\Pi(q^o)$. The ratio $(n-1)/n$ also measures how little a coordinating contract adds when many retailers compete (80% of the optimal profit at $n = 5$).

The results are proved in the chapter, mostly by short computations, and none of them has been machine-checked. The formalization makes explicit what the page leaves implicit: that no equilibrium has a retailer ordering zero, the limits behind "from 0 to 1", and the density condition behind the strict sign on p. 52. It also produces a reusable proportional-allocation game and a Nash-equilibrium predicate for nonnegative real strategies.

Difficulty

The algebraic identities (the profits at the coordinating contract, the ratio $(n-1)/n$, the derivative at $q^o$) are routine once $\pi_i$ has its closed form. The closed form itself requires computing the expectation with proportional shares and identifying $\mathbb E[\min(q,D)]$ with $q - \int_0^q F$.

The real obstacle is the uniqueness of the equilibrium. The page argues from first-order conditions, which describe only interior best responses. A complete proof must show that each retailer's profit is strictly concave in his own order, that no retailer orders zero in equilibrium, and that the all-zero profile (where $\pi_i$ has $q = 0$ in a denominator) is not an equilibrium. Strict concavity is the delicate step. The second derivative mixes the density with the term $\frac{2q_{-i}}{q^3}\big(qF(q) - \int_0^qF\big)$, and concavity has to be established on the closed half-line, including the boundary $q_i = 0$.

Formalization scope

Retailers are indexed by Fin n with $n \ge 2$ (the page's $n > 1$). The comparison in $n$ also allows a single retailer, as the page does. Orders are real numbers $q_i \ge 0$, and best responses range over all $x \ge 0$. The demand law is a probability measure on $\mathbb R$ carried by $[0,\infty)$ with finite mean, $F$ is its cdf, and $f$ is a field with HasDerivAt F (f y) y for $y > 0$. These are the chapter's standing assumptions (p. 7). The condition $c > 0$ is needed for (20) to have a solution. The integrated optimum $q^o$ enters each theorem through the hypothesis $F(q^o) = (p-c)/p$, which determines it uniquely. Transfers run from the retailers to the supplier.

Added or made explicit relative to the page: $b < p$ in the concavity claim (at $b = p$ the profit is linear); $f(q^o) > 0$ for the strict sign of the supplier's marginal profit; positivity of the total order wherever $\frac1q\int_0^qF$ appears. The page's printed slips (the first-order condition rescaled by $q^*/(p-b)$, "$F(q^o) = (p-c)/c$", "$w(b)$") are corrected in the statements and kept in the milestone quotes.

Ruled out as trivializing: $\widehat w$ and $w_b$ are the printed formulas, not "the price at which $q^o$ is an equilibrium"; the supplier's profit is computed from the transfers, not as $\Pi$ minus the retailers' profits; the equilibrium statement quantifies over all nonnegative deviations, so restricting attention to interior or symmetric profiles is not an option.

A complete development needs interval integrals of a cdf, the fundamental theorem of calculus for $q \mapsto \int_0^qF$, and strict concavity from a strictly decreasing derivative. The proportional-allocation game and the Nash predicate are reusable for the other allocation models of §6.5. No platform item is referenced: the competing-retailer game of Cachon and Lariviere (2005), RevShareCoord.Competing.*, uses deterministic revenue functions and is a different model.

Selected references

• G. P. Cachon, Supply Chain Coordination with Contracts, in S. Graves and T. de Kok (eds.), Handbooks in Operations Research and Management Science, vol. 11, North-Holland, 2003; read in the author's 3rd draft (Jan. 2003), §6.5.1. https://doi.org/10.1016/S0927-0507(03)11006-7
• Y. Wang and Y. Gerchak, Supply chain coordination when demand is shelf-space dependent, Manufacturing & Service Operations Management 3(1), 2001, 82–87. https://doi.org/10.1287/msom.3.1.82.9998
• S. A. Lippman and K. F. McCardle, The competitive newsboy, Operations Research 45(1), 1997, 54–65. https://doi.org/10.1287/opre.45.1.54
• S. Mahajan and G. van Ryzin, Inventory competition under dynamic consumer choice, Operations Research 49(5), 2001, 646–657. https://doi.org/10.1287/opre.49.5.646.10603
• G. P. Cachon and M. A. Lariviere, Supply chain coordination with revenue-sharing contracts: strengths and limitations, Management Science 51(1), 2005, 30–44. https://doi.org/10.1287/mnsc.1040.0215