Linear Optimization

Motivation

Linear programming algorithms often compute a solution to an auxiliary problem before extracting a solution to the original primal and dual pair. For a homogeneous self-dual formulation, the extraction requires a positive scaling coordinate. If that coordinate vanishes, the same auxiliary solution may instead describe infeasibility or unboundedness. Ye, Todd, and Mizuno introduced a homogeneous self-dual linear program that can start from arbitrary positive primal and dual slack vectors, even when the original programs have no known feasible point (Ye–Todd–Mizuno 1994).

Their Theorem 3 concerns strictly self-complementary optimal solutions of the auxiliary program. Theorem 9 addresses a different question: under a regularity assumption on the original programs, does a general optimal solution of the auxiliary program still have a positive scaling coordinate? The distinction matters because optimality alone does not require every complementary pair to have a positive member. This mission formalizes the statement of Theorem 9 and the numbered identities that frame it.

Setting

Fix a real matrix $A\in\mathbb R^{m\times n}$, a right-hand side $b\in\mathbb R^m$, and a cost vector $c\in\mathbb R^n$. The primal linear program (LP) minimizes $c^Tx$ subject to $Ax=b$ and $x\ge0$. Its dual (LD) maximizes $b^Ty$ subject to $A^Ty\le c$; $y\in\mathbb R^m$ is unrestricted. The dual slack is $s=c-A^Ty$.

An interior feasible point of (LP) is an $x$ with $Ax=b$ and every $x_j>0$. An interior feasible point of (LD) is a $y$ with every component of $c-A^Ty$ positive. “Interior” here is the paper's strict coordinatewise feasibility condition, not the topological interior of an equality-constrained set in ambient space. The existence of such a point implies ordinary feasibility for the corresponding program.

The paper builds an auxiliary program (HLP) from initial vectors $x^0>0$, $s^0>0$, and $y^0$. It uses the derived data

$$\bar b=b-Ax^0,\qquad \bar c=c-A^Ty^0-s^0,\qquad \bar z=c^Tx^0+1-b^Ty^0.$$

A point is a tuple $(y,x,\tau,\theta,s,\kappa)$ with $x,s,\tau,\kappa\ge0$ and free $y,\theta$. Its equality constraints are

$$\begin{aligned} Ax-b\tau+\bar b\theta&=0,\\ s&=-A^Ty+c\tau-\bar c\theta,\\ \kappa&=b^Ty-c^Tx+\bar z\theta,\\ -\bar b^Ty+\bar c^Tx-\bar z\tau&=-(x^0)^Ts^0-1. \end{aligned}$$

The objective is to minimize $((x^0)^Ts^0+1)\theta$. A feasible point is optimal when no feasible point has a smaller objective. The paper calls an optimal point self-complementary, whether or not its complementary pairs satisfy strict inequalities (p. 57, after Theorem 2(v)). After introducing the general construction, the paper fixes $y^0=0$ and $x^0=s^0=e$, the all-ones vector. That is the instance used in Theorem 9.

Formalization targets

Goal: Theorem 9

If both (LP) and (LD) have interior feasible points, then every self-complementary solution $w^*=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ of this fixed (HLP) satisfies

$$\tau^*>0.$$

The theorem quantifies over every optimal point, including those that are not strictly self-complementary. The printed tuple writes $\theta^*=0$; Theorem 2(iv) entails that fact from optimality, so it is not an extra hypothesis in the goal (Theorem 9, p. 64).

Supporting targets

Theorem 2(iv) states that (HLP) has zero optimal value and, for every feasible point under arbitrary positive initial $x^0,s^0$, satisfies

$$((x^0)^Ts^0+1)\theta=x^Ts+\tau\kappa.$$

Corollary 4 states that a positive $\kappa$ at an optimum under the fixed initialization entails infeasibility of (LP) or (LD). Equation (9) states the corresponding normalization identity

$$e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1.$$

These are separate milestone statements, each tied to its index and page in the paper (Theorem 2(iv), p. 57; equation (9), p. 58; Corollary 4, p. 59).

Significance

Theorem 9 says that the auxiliary model does not lose its positive scale at any optimum when the primal and dual programs are both strictly feasible. With $\tau^*>0$, the homogeneous primal and dual variables can be divided by $\tau^*$ to recover solutions in the original scale. The result applies even when the auxiliary optimum lacks strict complementarity; that is the additional coverage beyond the strictly self-complementary case of Theorem 3 (Ye–Todd–Mizuno 1994, pp. 58 and 64).

The mathematical result was proved in 1994. This mission's remaining work is a machine-checked proof of the stated regularity result and its supporting claims in the paper's specific (HLP) model. The definitions of the homogeneous feasible set, its slacks, and its optimality relation are reusable for the other results in the same paper. The full algorithm and complexity estimate belong to the other missions in this series.

Difficulty

The optimality condition controls the objective, and Theorem 2(iv) identifies that objective with a sum of complementarity terms. Those facts alone permit $\tau^*=0$; they do not force the scaling coordinate to be positive. Theorem 3's assertion for a strictly self-complementary point cannot be applied to an arbitrary optimal point, because its strict support condition may fail. The challenge is to use interior feasibility of both original programs to exclude all zero-scale optima while retaining the full set of HLP optima in the quantifier.

Formalization scope

The Lean model uses finite-dimensional real vectors indexed by Fin m and Fin n, a real matrix $A$, and a six-field HLP point in the paper's order $(y,x,\tau,\theta,s,\kappa)$. The standard-form primal and dual feasible sets are reused from a published LP definition with the same minimization and maximization orientation. Paper-specific interior predicates and the homogeneous program are defined locally. Slack fields in an HLP point are constrained to equal their formulas, so they cannot be chosen independently to make a statement true.

The model first defines (HLP) for general $x^0,y^0,s^0$ and then substitutes the paper's choice (7). It treats self-complementarity as objective minimization over the whole feasible set. Defining it by $\theta=0$ or by a complementarity equation would erase the content of Theorem 2(iv). The objective and normalization constants are exact, including the $n+1$ in the fixed instance. No real supremum or infimum is used to define optimality; it is a direct comparison against every feasible point.

The dimensions $m,n$ may be zero. Empty coordinatewise inequalities then have their usual vacuous meaning, but the equations remain in force. In particular the prescribed point $(0,e,1,1,e,1)$ is strictly feasible for every $A,b,c$, as a separate sorry-free local verification checks. This excludes an empty-feasible-set reading of the HLP definitions. Contributions proving the three numbered milestones, the goal, or reusable finite-dimensional LP lemmas are within scope.

Selected references

• Yinyu Ye, Michael J. Todd, and Shinji Mizuno, An $O(\sqrt nL)$-Iteration Homogeneous and Self-Dual Linear Programming Algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. DOI 10.1287/moor.19.1.53.

Motivation

Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form $Ax\ge b$ with $A\ge 0$: the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).

The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).

Setting

Fix integers $m\ge1$, $n$. Let $A$ be a real $m\times n$ matrix with nonnegative entries and rows $a_1,\dots,a_m$, write $a_ix=\sum_j A_{ij}x_j$, let $b\in\mathbb R^m$ with $b>0$, and let $P\subseteq\mathbb R^n$ be a nonempty convex set contained in the nonnegative orthant.

• COVERING asks whether there is $x\in P$ with $Ax\ge b$; such an $x$ is an exact solution. For $\varepsilon>0$, an $\varepsilon$-approximate solution is $x\in P$ with $Ax\ge(1-\varepsilon)b$.
• For $x\in\mathbb R^n$, $\lambda(x)=\min_i a_ix/b_i$ is the largest $\lambda$ with $Ax\ge\lambda b$, and $\lambda^*=\max\{\lambda(x):x\in P\}$. A point $x\in P$ is $\varepsilon$-optimal when $\lambda(x)\ge(1-\varepsilon)\lambda^*$.
• The width is $\max_i\max_{x\in P}a_ix/b_i$; a number $\rho>0$ with $a_ix\le\rho\,b_i$ for all $x\in P$ and all $i$ is a width bound.
• Subroutine (7) receives $y\in\mathbb R^m$, $y\ge0$, and returns $\tilde x\in P$ maximizing $y^tAx$ over $P$; $C_{\mathcal C}(y)$ is that maximum.
• For $\alpha>0$, the dual solution corresponding to $x$ is $y_i=\frac1{b_i}e^{-\alpha a_ix/b_i}$, and the potential is $\Phi=y^tb=\sum_ie^{-\alpha a_ix/b_i}$.
• The relaxed optimality conditions are $(\mathcal C1)$: $(1+\varepsilon)\lambda\,y^tb\ge y^tAx$, and $(\mathcal C2)$: $C_{\mathcal C}(y)-y^tAx\le\varepsilon\,(C_{\mathcal C}(y)+y^tb)$.
• IMPROVE-COVER$(x,\varepsilon)$ (Figure 3) sets $\lambda_0=\lambda(x)$, $\alpha=4\lambda_0^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$ and $\sigma=\varepsilon/(4\alpha\rho)$; while $\lambda(x)\le2\lambda_0$ and $\mathcal C2$ fails, it moves $x$ to $(1-\sigma)x+\sigma\tilde x$, $\tilde x$ the subroutine's answer for the current dual solution.
• The covering algorithm obtains a start with $Ax\ge\frac1mb$ from $m$ subroutine calls, calls IMPROVE-COVER with $\varepsilon=1/6$ until $\mathcal C2$ holds or an exact solution appears, then halves $\varepsilon$ phase by phase.

The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.

Formalization targets

Goal: Theorem 3.7 (p. 21)

For every instance as above, every width bound $\rho$, every exact maximization oracle and every $0<\varepsilon_0<1$, the covering algorithm stops after at most

$$N=m+\big(\lceil\log_2m\rceil+1\big)\big(2+4320\,\rho\ln(24m)\big)+2\lceil\log_2\varepsilon_0^{-1}\rceil+9408\,\rho\,\varepsilon_0^{-2}\ln\frac{24m}{\varepsilon_0}$$

calls to subroutine (7), and either returns $x\in P$ with $Ax\ge(1-\varepsilon_0)b$, or reports that no $x\in P$ has $Ax\ge b$, correctly. This is the paper's $O(m+\rho\log^2m+\varepsilon^{-2}\rho\log(m\varepsilon^{-1}))$ with the constants of its proof.

Milestones

In the order the proof uses them:

• Lemma 3.1: $\mathcal C1$ and $\mathcal C2$ imply that no exact solution exists if $\lambda\le1-3\varepsilon$, and that $x$ is $3\varepsilon$-optimal if $\lambda\ge1-3\varepsilon$.
• Lemma 3.2: if $\alpha\ge2\lambda^{-1}\varepsilon^{-1}\ln(4m\varepsilon^{-1})$, the dual solution corresponding to $x$ satisfies $\mathcal C1$.
• Lemma 3.3: while $\mathcal C2$ fails, a step of size $\sigma\le\varepsilon/(4\alpha\rho)$ lowers the potential: $\Phi-\hat\Phi\ge\varepsilon\alpha\sigma\Phi$.
• Lemma 3.4: during IMPROVE-COVER, $\lambda\ge\frac34\lambda_0$.
• Theorem 3.5: one call of IMPROVE-COVER makes at most $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ oracle calls, and at most $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ from a $6\varepsilon$-optimal start with $\varepsilon\le1/12$.
• Lemma 3.6: $m$ oracle calls give $x\in P$ with $Ax\ge\frac1mb$, or prove that no exact solution exists.

Significance

Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about $\rho\varepsilon^{-2}\log(m/\varepsilon)$ linear optimizations over $P$, plus lower-order terms in $m$. In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where $P$ is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.

The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.

Difficulty

The obvious argument tracks the potential $\Phi$ and stops when it is small. This does not work directly, because $\alpha$ is tied to $\lambda_0$, and the guarantee $\mathcal C1$ depends on $\lambda$ staying close to $\lambda_0$ throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition $\mathcal C2$ is not scaled by $\lambda$, so $\mathcal C1$ and $\mathcal C2$ give $\varepsilon$-optimality only when $\lambda$ is near $1$; the first phase must first raise $\lambda$ from $1/m$ by repeated doubling. And the cost of $\varepsilon$-scaling is bounded only because each phase starts from a $6\varepsilon$-optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit $N$, over a fuel-bounded run, is substantial.

Formalization scope

Rows are Fin m with [NeZero m], coordinates Fin n; $A$ is a Matrix (Fin m) (Fin n) ℝ; $P$ is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. $\lambda(x)$ is a Finset.inf' over the rows. Conventions committed to:

• Width. $\rho$ is any upper bound with $\rho>0$, not a supremum; the theorems hold for every such bound, the exact width included.
• Oracle. Subroutine (7) is a function that, for every $y\ge0$, returns a maximizer of $y^tAx$ over $P$; every theorem quantifies over all such functions. Box (7) of the report prints "min", but every use maximizes; the maximizer reading is adopted.
• Optimality without $\lambda^*$. "$x$ is $c\varepsilon$-optimal" is stated as $(1-c\varepsilon)\lambda(x')\le\lambda(x)$ for every $x'\in P$.
• Runs. IMPROVE-COVER and the driver are fuel-bounded functions returning some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the $\mathcal C2$ check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel $\lceil N\rceil$ stops; it does not assume termination.
• Driver. The prose of pp. 20–21 is written down as initCover, firstPhase and scalingPhases with $\varepsilon_k=\frac16 2^{-k}$.
• Constants replacing $O(\cdot)$. Theorem 3.5: $2+20\rho\varepsilon^{-3}\ln(4m/\varepsilon)$ and $2+196\rho\varepsilon^{-2}\ln(4m/\varepsilon)$ oracle calls. Theorem 3.7: the $N$ above.
• Implicit hypotheses made explicit. $y\ne0$ and $\varepsilon<\frac13$ in Lemma 3.1; $\lambda>0$ in Lemmas 3.2–3.4 and Theorem 3.5; $\sigma\ge0$ in Lemma 3.3.
• Misprint. Theorem 3.5's second sentence names IMPROVE-PACKING; it is stated for IMPROVE-COVER.

A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.

A complete development needs elementary real analysis (the second-order bound $e^{x+\delta}\le e^x+\delta e^x+\frac\varepsilon2|\delta|e^x$ for $|\delta|\le\varepsilon/4$), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.

Selected references

• S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Cornell University School of ORIE Technical Report No. 999, February 1992. https://core.ac.uk/download/79020349.pdf
• S. A. Plotkin, D. B. Shmoys, É. Tardos, Fast Approximation Algorithms for Fractional Packing and Covering Problems, Mathematics of Operations Research 20(2), 257–301, 1995. https://doi.org/10.1287/moor.20.2.257
• N. Garg, J. Könemann, Faster and Simpler Algorithms for Multicommodity Flow and Other Fractional Packing Problems, SIAM Journal on Computing 37(2), 630–652, 2007. https://doi.org/10.1137/S0097539704446232
• N. E. Young, Sequential and Parallel Algorithms for Mixed Packing and Covering, Proc. 42nd IEEE FOCS, 538–546, 2001. https://arxiv.org/abs/cs/0110040

Motivation

Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far apart the two quantities can be. Leighton and Rao (J. ACM 46 (1999), extending their FOCS 1988 paper) proved that for uniform demands the gap is at most logarithmic in the number of nodes, and turned the proof into approximation algorithms for a range of NP-hard cut problems.

Their §2.4 extends the result to directed networks, where every edge carries flow in one direction only. The directed version is the one behind their approximation algorithms for directed problems, most prominently the minimum feedback arc set problem (§3 of the paper), where the cut structure of a digraph, not of its underlying undirected graph, is what matters.

Timeline. Ford and Fulkerson (1956): max-flow = min-cut for one commodity. Hu (1963): equality for two commodities in undirected graphs. Shahrokhi and Matula (1990, circulated 1986): the uniform concurrent flow problem and its LP dual. Leighton and Rao (FOCS 1988; J. ACM 1999): $\Omega(\mathcal S/\log n)\le f\le\mathcal S$ for uniform and product demands, undirected and directed, tight up to the constant for undirected uniform problems. Klein, Rao, Agrawal and Ravi (1990s) and Linial, London and Rabinovich (1995) extended the undirected theorem to general demands with an $O(\log k)$ gap. For directed graphs with general demands the gap is polynomial in $n$ (Chuzhoy and Khanna 2009), so the uniform-demand directed theorem is the setting where a logarithmic gap holds.

Setting

A directed network is a finite vertex set $V$ with $n=|V|$ nodes and a capacity $C(u,v)\ge0$ for each ordered pair, with $C(u,u)=0$; there is an edge directed from $u$ to $v$ when $C(u,v)>0$. For $U\subseteq V$ write $\bar U=V\setminus U$ and let $C(U,\bar U)=\sum_{u\in U,\,v\in\bar U}C(u,v)$ be the capacity of the edges directed from $U$ to $\bar U$.

The directed uniform multicommodity flow problem (directed UMFP) has one commodity for every ordered pair $(u,v)$ with $u\ne v$, each with demand $1$. A concurrent flow of value $\lambda$ routes $\lambda$ units of every commodity simultaneously, each edge carrying flow only in its own direction, with total flow on the edge $u\to v$ at most $C(u,v)$. The max-flow $f$ is the largest such $\lambda$.

The ratio cost of a cut is $C(U,\bar U)/(|U|\,|\bar U|)$, and the min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

A distance function assigns a length $d(u,v)\ge0$ to each directed edge; $d(u,v)$ then also denotes the length of a shortest directed path from $u$ to $v$, its total weight is $W=\sum_{u,v}C(u,v)\,d(u,v)$, and the distance constraint is $\sum_{(u,v)\in V^2}d(u,v)\ge1$. The sets $\mathcal N^\Delta_{\mathrm{in}}(v,G)$ and $\mathcal N^\Delta_{\mathrm{out}}(v,G)$ are the nodes from which $v$ can be reached, respectively which can be reached from $v$, by a directed path of length at most $\Delta$. Logarithms are to base $2$.

In Lean these are DiNetwork, diCutCap, diRatio, diMinCut, diDemand, IsDiConcurrentFlow, diMaxFlow, diDist, diTotalWeight, SatisfiesDiConstraint, inBall and outBall, in the namespace LeightonRao.Directed.

Formalization targets

Goal: Theorem 12 (p. 804)

There is an absolute constant $c>0$ such that every directed UMFP on $n\ge2$ nodes satisfies

$$c\,\frac{\mathcal S}{\log n}\le f\le\mathcal S.$$

The constant is left unfixed, as in the paper's $\Omega(\cdot)$; any improvement of the constant leaves the goal intact.

Milestones

1. Weak duality (p. 804): every concurrent flow of value $\lambda$ has $\lambda|U||\bar U|\le C(U,\bar U)$ for every proper cut.
2. LP duality (§2.2, p. 796, used for directed graphs in §2.4): every feasible distance function has $W\ge f$, and an optimal one has $W=f$.
3. Lemma 13 (p. 804): for every $\Delta>0$, an ordered partition $V_1,\dots,V_r$ whose backward edges (from $V_i$ to $V_j$, $j<i$) have capacity at most $8W\log n/\Delta$, each part containing a node whose in- and out-balls of radius $\Delta$ are at least as large as the part.
4. Corollary 14 (p. 806): with $\Delta=1/4n^2$, either a node whose in- and out-balls both have at least $2n/3$ nodes, or a directed cut of ratio cost at most $8W\log n/(\Delta(n/6)(5n/6))$.
5. Lemma 15 (p. 806): a set $T$ with $|T|\ge2n/3$ and $\sum_{u\notin T}d(T,u)\ge1/4n$ or $\sum_{u\notin T}d(u,T)\ge1/4n$ gives a directed cut of ratio cost at most $12W$.
6. Lemma 16 (p. 807): a distance function satisfying the distance constraint gives a directed cut of ratio cost at most $\tfrac{1152}{5}W\log n$.

Significance

The result. Theorem 12 says that the directed sparsest cut and the directed uniform concurrent flow agree within an $O(\log n)$ factor. Since the flow is an LP, this gives an $O(\log n)$-approximation for the directed uniform sparsest cut, and through divide and conquer, polylogarithmic approximations for directed problems such as minimum feedback arc set and minimum directed cut linear arrangement (§3 of the paper). It is also the case in which a logarithmic flow–cut gap survives for digraphs: with arbitrary demands, the directed gap is polynomial.

Formalizing it. The theorem has been proved since 1988, but no part of it is formalized: Mathlib has no multicommodity flows, no directed path metrics over real lengths, and no region-growing arguments. This mission produces the directed concurrent-flow model, its LP duality, and the directed region-growing decomposition of Lemma 13, each reusable beyond this paper (directed multicut, feedback arc set, low-diameter decompositions of digraphs).

Difficulty

The obvious route copies the undirected proof: grow a ball around a node until the capacity on its boundary is small compared with the capacity inside, cut it off, and repeat. In a digraph this fails at two places. A ball of small out-radius can have large in-radius, so a piece cut off by out-distances is not small in the sense needed later; and cutting off a piece only controls the edges leaving it in one direction, so edges pointing back into earlier pieces are not paid for. Lemma 13 has to bound the capacity of all backward edges of an ordered partition while keeping each part inside both an in-ball and an out-ball around one of its own nodes. The final averaging step also changes: the undirected argument sums $d(T,u)+d(T,v)$ over symmetric pairs, which has no directed counterpart, so the distance constraint over ordered pairs has to be split between distances into one set and out of another.

Formalization scope

Vertices form a Fintype with decidable equality, and every goal-level statement assumes $n\ge2$. Commodities are ordered pairs with demand $1$; a flow is in arc form, $f_{st}(i,j)\ge0$ with conservation, and the capacity constraint is per directed edge. The max-flow is the supremum (sSup) of the achievable values $\lambda\ge0$; the min-cut is an infimum over nonempty proper subsets, since the ratio is $0/0$ otherwise. Shortest-path distances are infima over directed walks (lists of vertices along edges of positive capacity); for nonnegative lengths these equal shortest-path lengths. An unreachable pair would get Lean's junk value $0$, so every statement using $d(u,v)$ assumes strong connectivity ($C(U,\bar U)>0$ for every proper $U$), the directed analogue of the paper's standing assumption on p. 789; the balls are defined through the existence of a walk and need no such assumption. $W$ counts each directed edge once, and the distance constraint sums over ordered pairs. "We can find" is read as existence; running times are not formalized. The $\Omega$ of Theorem 12 is one absolute constant chosen before the network; the explicit constants $8$, $1152/5$ and $12$ of the milestones are the ones computed in the paper's proofs.

Two printed slips are corrected and disclosed: Lemma 13 (1) prints $1\le j<i<r$ where the proof uses $i\le r$, and the proof's last line prints $|\mathcal N^\Delta_{\mathrm{out}}(v,G)|\le|V_i|$ where the statement has $\ge$.

The statement cannot be trivialized by a degenerate cut or flow: cuts range over nonempty proper subsets, the flow's capacity constraint is directional, and the goal's constant is quantified before the network, so a constant depending on $n$ does not count.

Needed infrastructure: LP duality for the concurrent flow LP (or a direct proof of the max-flow/distance duality), shortest directed paths with real lengths, and the region-growing bookkeeping. Contributions to any milestone are welcome, as are alternative proofs of Lemma 13 by continuous region growing.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
• N. Linial, E. London and Yu. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• J. Chuzhoy and S. Khanna, Polynomial flow-cut gaps and hardness of directed cut problems, J. ACM 56(2):6, 2009. https://doi.org/10.1145/1502793.1502795

Why multicommodity max-flow and min-cut

For a single commodity, the Ford–Fulkerson theorem says that the maximum flow between two nodes equals the minimum capacity of a cut separating them. Many routing and partitioning problems involve many source–sink pairs at once, and for those the equality fails: the largest fraction of every demand that can be routed simultaneously can be strictly smaller than the sparsest cut. Leighton and Rao (J. ACM 1999, building on their FOCS 1988 paper) proved that the gap is at most logarithmic for broad classes of demand patterns, and turned the proof into the first $O(\log n)$-approximation algorithms for sparsest cut, balanced separators, minimum feedback arc set, crossing number and VLSI layout problems.

This mission formalizes Section 2.3 of the paper: the extension of the uniform max-flow min-cut theorem to product multicommodity flow problems (PMFPs), where the demand between two nodes is the product of their node weights.

Timeline.

• 1956: Ford and Fulkerson, single-commodity max-flow = min-cut.
• 1963: Hu, equality for two commodities.
• 1988: Leighton and Rao (FOCS), $\Theta(\log n)$ gap for uniform demands; the product-demand extension, pointed out to them by Shmoys, Tardos and Sinclair, appears in the journal version (1999), Theorem 7.
• 1993–1995: Klein–Agrawal–Ravi–Rao, Garg–Vazirani–Yannakakis, Linial–London–Rabinovich and Aumann–Rabani extend the $O(\log k)$ gap to arbitrary demands with $k$ commodities.

Setting

A network is a finite vertex set $V$ with a symmetric capacity $C(u,v)\ge0$ on each pair, zero on the diagonal; $\{u,v\}$ is an edge when $C(u,v)>0$. For $U\subseteq V$, the cut capacity is $C(U,\bar U)=\sum_{u\in U,\,v\notin U}C(u,v)$. The network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$.

A PMFP is given by a node weighting $\pi:V\to\mathbb R_{\ge0}$. Write $\mathcal P$ for the set of nodes with $\pi(u)\ne0$, $p=|\mathcal P|$, and $\pi(U)=\sum_{u\in U}\pi(u)$. As in the paper, the weights are normalized so that $\pi(V)=p$. Every pair $\{u,v\}$ is a commodity with demand $\pi(u)\pi(v)$; there are $k=\binom p2$ commodities with nonzero demand. The uniform problem is $\pi\equiv1$.

The max-flow $f$ is the largest $\lambda$ such that $\lambda\pi(u)\pi(v)$ units of every commodity can be routed simultaneously, with the total flow on each edge (both directions) at most its capacity. The min-cut is

$$\mathcal S=\min_{U:\ \pi(U)>0,\ \pi(\bar U)>0}\frac{C(U,\bar U)}{\pi(U)\,\pi(\bar U)},$$

the quotient being the weighted ratio cost of the cut $\langle U,\bar U\rangle$.

The dual objects are distance functions: lengths $d(e)\ge0$ on the edges, with total weight $W=\sum_eC(e)d(e)$; $d(u,v)$ is the shortest-path distance and $d(T,u)=\min_{t\in T}d(t,u)$. The weighted distance constraint is $\sum_{\{u,v\}\in\mathcal P^2}\pi(u)\pi(v)d(u,v)\ge1$.

Formalization targets

Goal: Theorem 7 (pp. 801–802)

There is an absolute constant $c>0$ such that every normalized PMFP with $p\ge2$ on a connected network satisfies

$$\frac{c\,\mathcal S}{\log_2\max(k,2)}\le f\le\mathcal S .$$

The goal leaves the constant unfixed, which is the paper's $\Omega(\cdot)$.

Milestones, in the order the proof uses them

1. Weak duality (§1.2, pp. 789–790): $f\,\pi(U)\pi(\bar U)\le C(U,\bar U)$ for every cut with positive weight on both sides.
2. LP duality for the PMFP (p. 802 with p. 796): distance functions satisfying the weighted constraint have $W\ge f$, and one attains $W=f$.
3. Lemma 8 (p. 802): a partition whose components meeting $\mathcal P$ have radius at most $\Delta$ and whose cross capacity is at most $4W\log p/\Delta$.
4. Corollary 9 (p. 802): either a set $T$ of radius $1/2p^2$ with $\pi(T)\ge2p/3$, or a cut of weighted ratio cost $O(W\log p)$.
5. Lemma 10 (p. 802): a heavy set $T$ far on average from the remaining weight yields a cut of weighted ratio cost $O(W)$.
6. Lemma 11 (p. 803): a distance function satisfying the weighted constraint yields a cut of weighted ratio cost $O(W\log p)$.

Stronger companions

• $\mathcal S\le36\log_2\max(k,2)\cdot f$, the constant of the paper's proof.
• Theorem 7 without the normalization $\pi(V)=p$, which the paper assumes "without loss of generality".

Significance

Theorem 7 bounds the multicommodity flow–cut gap by $O(\log k)$ for every product demand pattern, so an optimal dual distance function certifies a cut within $O(\log k)$ of the sparsest weighted cut. The paper itself applies it to reversible Markov chains (§3.27, p. 827). There the node weights are the stationary probabilities, and Theorem 7 shows that the inverse conductance and the resistance of a chain agree up to a $\Theta(\log p)$ factor, where $p$ is the number of states with positive stationary probability.

Theorem 7 was proved in 1988–1999 and is subsumed, up to the constant, by the general $O(\log k)$ bound for arbitrary demands (Linial–London–Rabinovich 1995; Aumann–Rabani 1998). It has no machine-checked proof, and neither has any of its milestones. A complete development would also be the first formal treatment on Prove2Me of concurrent multicommodity flow, its LP dual, and region-growing (low-diameter) decompositions, which recur across approximation algorithms and metric embeddings.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the work. Rounding an optimal dual distance function to a cut fails directly: thresholding distances from a single node gives no control on the ratio when the weight is spread out. The paper's argument needs a decomposition of the graph into components of small radius that cuts little capacity, with a loss of only $\log p$, not $\log n$: the regions must be grown from weighted nodes only, while the many zero-weight nodes still sit inside the graph and its capacities. It must then separately handle the case where one component carries two thirds of the weight. Formally, the LP duality step alone requires a strong-duality statement for a linear program with one constraint per path, exponentially many, which Mathlib does not provide in this form.

Formalization scope

All objects live in the namespace LeightonRao.Product in a single definitions file.

• Network and graph. A network is a symmetric nonnegative capacity function on a finite type with zero diagonal. The graph has an edge where the capacity is positive.
• Commodities. One commodity per ordered pair $u\ne v$, with demand $\tfrac12\pi(u)\pi(v)$ each way (the paper's footnote 7). The total demand of a pair is then $\pi(u)\pi(v)$, and the demand separated by $U$ is $\pi(U)\pi(\bar U)$.
• Max-flow. Flows are arc flows per commodity. The max-flow is the supremum of the feasible values $\lambda\ge0$.
• Min-cut. The min-cut ranges only over cuts with $\pi(U)>0$ and $\pi(\bar U)>0$. On the other cuts the paper's quotient is undefined; reading it with Lean's division by zero would make $\mathcal S=0$ and the goal trivial.
• Distances, radius, cross capacity. Graph distances are infima of walk lengths. The radius of a component is measured by walks inside the component. Cross capacity is the capacity between different parts of a Finpartition.
• Logarithms. $\log$ is $\log_2$ (the paper's footnote 3). For $p=2$ there is one commodity and $\log k=0$, so the goal uses $\log_2\max(k,2)$.
• Constants. The $O(\cdot)$ constants of the milestones are the ones computed in the paper's proofs: $36$ in Corollary 9 and Lemma 11, $6$ in Lemma 10.
• Hypotheses added to the page, each disclosed in its statement:
  • $\Delta>0$ in Lemma 8, where the page says $\Delta\ge0$ but divides by $\Delta$;
  • $p\ge2$ in Lemma 8, which is false for $p=1$;
  • the weighted ratio cost in Lemma 10, as its proof and its use in Lemma 11 require.
• Not formalized. The polynomial-time content of "we can find" is not formalized; each such claim is an existence statement.

Contributions are welcome at every level:

• proofs of the milestones;
• a general strong-duality lemma for concurrent flow, reusable for the uniform, directed and short-path missions of this series;
• a reusable region-growing decomposition lemma.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• T. Leighton and S. Rao, An approximate max-flow min-cut theorem for uniform multicommodity flow problems with applications to approximation algorithms, FOCS 1988, 422–431. https://doi.org/10.1109/SFCS.1988.21958
• N. Garg, V. V. Vazirani and M. Yannakakis, Approximate max-flow min-(multi)cut theorems and their applications, SIAM J. Comput. 25(2):235–251, 1996. https://doi.org/10.1137/S0097539793243016
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• Y. Aumann and Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27(1):291–301, 1998. https://doi.org/10.1137/S0097539794285983
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620

Motivation

A finite Markov decision process may have several recurrent classes under one policy. In that setting, its long-run reward depends on the initial state, and a single stationary distribution does not describe the whole decision problem. Hordijk and Kallenberg developed a linear program with two families of variables to handle this multichain case. Their Theorem 8 relates policies to feasible points of that program in both directions: optimal stationary policies give optimal dual solutions, and every optimal dual solution gives an average optimal stationary policy. This relationship explains why the dual program represents the original sequential decision problem rather than merely bounding its value. Hordijk and Kallenberg (1979)

An earlier frequency formulation associated stationary randomized policies with one family of occupation variables in a more restricted Markov-chain setting. The present theorem uses both $x$ and $y$ variables, and its policy comparison covers history-dependent randomized decisions. The corresponding formalization therefore addresses the finite multichain model of the 1979 paper, with its own dual equations and representative map. Hordijk and Kallenberg (1979), §§1 and 3.3

Setting

Let $E$ be a nonempty finite set of states. At state $i$, an action $a$ is chosen from a nonempty finite set $A(i)$. It earns a real reward $r_{ia}$ and moves to state $j$ with probability $p_{iaj}$. The transition probabilities are nonnegative and sum to one over $j$. A general policy $R$ may randomize and use the complete past history. Its average reward $\phi_i(R)$ is the liminf, as the horizon grows, of expected total reward divided by the horizon when the initial state is $i$. The optimal value $\phi_i$ is the supremum of $\phi_i(R)$ over all such policies. A policy is average optimal when it attains that value at every state. These are the conventions of §2.1 of the paper. Hordijk and Kallenberg (1979), p. 353

A stationary randomized policy $\pi^\infty$ chooses each admissible action $a$ at state $i$ with a fixed probability $\pi_{ia}$, independently of the epoch and history. Its transition matrix is $P(\pi)_{ij}=\sum_{a\in A(i)}\pi_{ia}p_{iaj}$, and its reward vector is $r(\pi)_i=\sum_{a\in A(i)}\pi_{ia}r_{ia}$. The Cesàro limit matrix $P^*(\pi)$ and deviation matrix $D(\pi)$ describe the recurrent and transient behavior of this finite chain. In particular, $\phi(\pi^\infty)=P^*(\pi)r(\pi)$. Hordijk and Kallenberg (1979), p. 359

Fix positive state weights $\beta_j$ summing to one. The primal linear program minimizes $\sum_j\beta_j\widetilde\phi_j$ over pairs $(\widetilde\phi,\widetilde u)$ that are superharmonic: for every $i$ and $a\in A(i)$, the first vector dominates its one-step expected continuation, and the sum of the two vectors dominates one-step reward plus the continuation of the second. The dual linear program maximizes $\sum_{i,a}r_{ia}x_{ia}$ over nonnegative $x_{ia}$ and $y_{ia}$ satisfying the two flow equations (3) and (4). Variables are present only for admissible state-action pairs. The set $E_x$ consists of states where $\sum_a x_{ia}>0$. Hordijk and Kallenberg (1979), pp. 356–357

For a feasible dual point $(x,y)$, the associated policy $\pi(x,y)$ normalizes the $x$ row at states in $E_x$ and the $y$ row at other states. Conversely, equation (6) constructs a representative $(x(\pi),y(\pi))$ of a stationary randomized policy. Its $x$ coordinates use $\beta^TP^*(\pi)$. Its $y$ coordinates use $\beta^TD(\pi)+\gamma^TP^*(\pi)$, where $\gamma$ is zero at transient states and is chosen separately on each recurrent class by a maximum formula. The formalization restricts that formula's denominator to the recurrent class, as required by the subsequent nonnegativity calculation; the printed unrestricted denominator has a two-state counterexample. Hordijk and Kallenberg (1979), pp. 359–360

Formalization targets

Optimality correspondence

The goal is Theorem 8, with both directions in one statement:

$$\pi^\infty\text{ average optimal}\ \Longrightarrow\ (x(\pi),y(\pi))\text{ dual optimal}, \qquad (x,y)\text{ dual optimal}\ \Longrightarrow\ \pi^\infty(x,y)\text{ average optimal}.$$

The second implication applies to every optimal dual point. It produces the stationary randomized policy given by the printed normalization rule, including its existence as a valid policy. The first implication uses the particular representative defined by equation (6). Neither direction imposes an extreme-point condition. Hordijk and Kallenberg (1979), Theorem 8, p. 360

Supporting results

The milestones state the least-superharmonic characterization of $\phi$; the positivity that makes the dual-to-policy normalization meaningful; the stationary gain identity; feasibility and objective value of the representative; and Propositions 4 and 5, which describe tight actions and identify $E_x$ with the recurrent states of $P(\pi(x,y))$. Each is a statement about the same finite model and the same primal–dual pair. Hordijk and Kallenberg (1979), pp. 356–361

Significance

The theorem establishes an exact relation between two ways of expressing average optimality. The LP direction turns an optimal stationary policy into a dual optimum with a concrete state-action representation. The converse says an arbitrary optimal dual point can be read as an average optimal policy, even when its $x$ coordinates vanish at some states. Proposition 5 specifies what those vanishing coordinates mean for the induced chain: those states are transient. These statements permit optimization over a finite LP while preserving the policy interpretation of its solutions. Hordijk and Kallenberg (1979), Theorem 8 and Proposition 5

The result was proved in 1979; this mission asks for a machine-checked proof of its precise finite-state statement. The shared MDP model and the limit and deviation matrix definitions already exist as published formal objects. The new work is the correspondence for Hordijk and Kallenberg's dual equations, with the representative, its class-wise correction, and the connection to liminf average reward. The definitions of stationary policy mixtures, admissible-pair LP coordinates, and finite-chain recurrence can support later results about average-reward optimization.

Difficulty

Normalizing $x$ alone does not define a policy at every state: its row sum can be zero. The dual program's second variable $y$ supplies the action weights there, and the feasibility equations must ensure its row sum is positive. In the other direction, the natural $\beta^TD(\pi)$ term in $y(\pi)$ need not be nonnegative. The correction $\gamma$ is chosen by a maximum over each recurrent class, while transient states require a different case. These issues remain in a multichain process even though the state and action sets are finite. Hordijk and Kallenberg (1979), pp. 359–361

Formalization scope

Lean uses finite types for states and actions, a nonempty state type, and a nonempty admissible action set at every state. The published StationaryMDP definition provides real rewards and stochastic transition rows. General policies are its history-dependent randomized AvgHRPolicy values; average reward is its liminf reward, and optimal gain is the supremum over that entire policy class. The mission defines its own average-optimality predicate because the published Puterman predicate uses a stronger limsup comparison. For finite rewards, the liminf gains and their supremum are bounded real numbers.

Stationary randomized weights are nonnegative, sum to one on each $A(i)$, and vanish outside $A(i)$. The dual variables are functions on the subtype of admissible state-action pairs. The primal and dual optima mean feasible points attaining the relevant objective against every other feasible point. The paper's positive, normalized $\beta$ remains explicit. The raw formula for $\pi(x,y)$ is used only with a feasible dual point, and the policy-well-definedness milestone supplies its nonzero denominators. The representative uses a maximum over the ergodic class of each recurrent state, with the class-restricted denominator needed by the paper's proof; replacing $\gamma$ by zero or by one global maximum would change the target.

The known matrix objects $P^*$ and $D$ are imported from the published Blackwell development. Their convergence and identities are theorem obligations, not assumptions hidden in definitions. Contributions proving the finite-chain identities, representative feasibility, complementary slackness, and the final policy comparison are within scope. A statement restricted to a unichain model, an extreme dual point, or a pure selected action would not establish this theorem.

Selected references

• A. Hordijk and L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. DOI: 10.1287/mnsc.25.4.352.

Motivation

Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6

Setting

Fix a dimension $n$, an integer $d$ with $0\le d\le n$, and a vector $r\in\mathbb R^n$. Draw a random $d$-dimensional subspace $U$ from the distribution invariant under orthogonal transformations. Let $p$ be the Euclidean orthogonal projection of $r$ onto $U$, and put $q=r-p$, its projection onto $U^\perp$. The matrix $P=\operatorname{diag}(p)$ turns the vector $q$ into the coordinatewise product $Pq=(p_jq_j)_{j=1}^n$.

For a coordinate vector $z$, let $z^-=(\min\{z_j,0\})_{j=1}^n$ and $\|z\|^-_\infty=\|z^-\|_\infty$. Thus $\|Pq\|^-_\infty$ records the magnitude of the largest negative coordinate of $Pq$. An unsubscripted vector norm is always the Euclidean $\ell_2$ norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2

The formal model samples an $(n-d)\times n$ matrix $G$ with independent standard normal entries and sets $U=\ker G$. The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension $d$. The construction covers the endpoint cases $d=0$ and $d=n$ as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6

Formalization targets

Theorem 5

For arbitrary choices $r_n\in\mathbb R^n$ and $d_n\le n$ at each dimension, the central target is

$$\Pr\left\{\|P_nq_n\|^-_\infty\le \frac{\log n}{n}\|r_n\|_2^2\right\} \longrightarrow 1\qquad(n\longrightarrow\infty).$$

The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of $r_n$ and $d_n$ may change with $n$; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13

Source milestones

The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by $\sqrt{3\log n/n}$ with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6

Significance

The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7

The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.

Difficulty

A direct norm bound on $p$ and $q$ loses the coordinate information needed for the factor $\log n/n$. The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), so $\|r\|$ is the $\ell_2$ norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated $d$-dimensional law almost surely.

Lemma 6 concerns $d,m\ge1$ and $n\ge2$, where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains $d=0$, $d=n$, and $r=0$. Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition $\varepsilon>0$. All limits are probabilities tending to one, never probability one at every finite $n$.

Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.

Selected references

• Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. DOI
• Sidney I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71, cited in the report for the Gaussian maximum estimate. DOI

Motivation

Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.

Timeline of the LP approach to average-cost problems:

• 1960 — Manne: the inventory model as a linear program in the joint probabilities of (stock level, production quantity); mixed strategies allowed; the decision rule is read off as a conditional probability.
• 1960 — H. M. Wagner, in a companion note in the same issue, shows that an optimal solution consisting of pure strategies exists.
• 1962 — C. Derman (Management Science 9(1), 1962) gives the general finite-state, finite-action version, assuming every stationary randomized rule yields an irreducible chain.
• 1960 — F. d'Epenoux (Revue Française de Recherche Opérationnelle 4, No. 14; English translation 1963) treats the discounted criterion by linear programming, as Manne's closing note records.

Setting

A positive integer $T$ bounds inventory accumulation; the stock levels are $0,1,\dots,T$. At the start of a month the initial stock $i$ is observed and a production quantity $j$ is chosen; the available stock is $k=i+j$. The month's demand $n\in\{0,1,2,\dots\}$ is independent of everything else and has law $p_n$. Backlogs are excluded, so the terminal stock is $t=\max(0,k-n)$, which becomes the next initial stock. A finite set $A$ of admissible pairs $(i,j)$, all with $i+j\le T$ and containing $(i,0)$ for every $i\le T$, lists the decisions available at each stock level. Costs are three arbitrary real functions: $C_1(i)$ of the initial stock, $C_2(j)$ of the production quantity, and $C_3(n-k)$ of the shortage level.

A stationary randomized decision rule $q(j\mid i)$ is a conditional probability of producing $j$ at stock $i$, supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of $q$ is a stationary distribution $y=(y_0,\dots,y_T)$ of that chain: the law $y'$ of the terminal stock equals the law $y$ of the initial stock, (2). The expected monthly cost (1) of $q$ in the equilibrium $y$ is

$$\mathcal EC_1(i)+\mathcal EC_2(j)+\mathcal EC_3(n-k),$$

the expectation taken under the joint law $y_i\,q(j\mid i)\,p_n$ of (initial stock, production, demand).

The linear program has one unknown $x_{ij}$ per admissible pair, the joint probability of (initial stock $i$, production $j$). Its constraints are $x_{ij}\ge0$, (4) $\sum_{i,j}x_{ij}=1$, and the equilibrium equations

$$\text{(8.t)}\qquad \sum_j x_{tj}=\sum_{\substack{i,j,n:\\ i+j-n=t}}p_nx_{ij}\qquad(t=1,\dots,T),$$

and its objective (9) is $\sum_{i,j}c_{ij}x_{ij}$ with the cost coefficients (10)

$$c_{ij}=C_1(i)+C_2(j)+\sum_np_nC_3(n-i-j).$$

The companion equation (8.0) for $t=0$ has right-hand side $\sum_{i+j-n\le0}p_nx_{ij}$ and is omitted from the constraints. A feasible $x$ is decoded into $y_i=\sum_jx_{ij}$ and $q(j\mid i)=x_{ij}/y_i$.

Formalization targets

The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.

Goal: an LP optimum gives an optimal stationary rule

Assume $\sum_np_n|C_3(n-i-j)|<\infty$ for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution $x^*$, with decoding $(q^*,y^*)$, $q^*$ is a stationary randomized rule, $y^*$ is a statistical equilibrium of $q^*$, and

$$\mathrm{Cost}(q^*,y^*)=\sum_{i,j}c_{ij}x^*_{ij}\le \mathrm{Cost}(q,y)$$

for every stationary randomized rule $q$ and every statistical equilibrium $y$ of $q$.

Milestones

1. (7): under a rule in a distribution $y$, the law of the terminal stock is the right-hand side of (7)/(8) evaluated at $x_{ij}=y_iq(j\mid i)$.
2. (8.0)–(8.T): a rule in statistical equilibrium yields a point satisfying $x\ge0$, (4) and all of (8.0)–(8.T).
3. (8.0) is redundant: (4) and (8.1)–(8.T) imply (8.0).
4. §3, N.B.: every feasible $x$ equals $y_iq(j\mid i)$ for its decoding $(q,y)$, with $y$ an equilibrium of $q$.
5. (10): the expected monthly cost (1) under the joint law $x_{ij}p_n$ equals $\sum c_{ij}x_{ij}$.
6. Table 1: the cost coefficients of the §6 example ($T=3$, $p=(2/3,0,1/3)$, $C_1(i)=i$, $C_2(j)=3j$, $C_3(m)=\max[0,6m]$, $j\in\{0,1\}$) are $4,5,3,4,2,5,3$.
7. Table 2, footnote 3: $x_{01}=1/3$, $x_{11}=2/9$, $x_{20}=4/9$ is optimal with cost $31/9$; the do-nothing solution costs $4$.
8. Footnote 5: the implicit prices $-7/3,-13/3,-11/3$ of (8.1)–(8.3), with $31/9$ on (4), are an optimal dual solution.

Significance

The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.

The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient $x_{ij}/\sum_jx_{ij}$ is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.

Difficulty

Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over $(i,j,n)$ with conditions $i+j-n\le0$ and $i+j-n=t$, and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and $\sum_np_n=1$. The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level $0$ must be recovered from (4) and the bound $i+j\le T$. And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.

Formalization scope

All statements live in the namespace ManneLP.Equilibrium. Conventions:

• Stock levels and production quantities are natural numbers; a model carries $T>0$, the admissible set $A$ (a Finset (ℕ × ℕ) with $i+j\le T$ and every $(i,0)\in A$), a demand law $p:\mathbb N\to\mathbb R$ with $p_n\ge0$ and HasSum p 1, and costs $C_1,C_2:\mathbb N\to\mathbb R$, $C_3:\mathbb Z\to\mathbb R$. The shortage level $n-i-j$ is an integer; no convexity, sign or monotonicity of the costs is assumed.
• The admissible set is a parameter: §6 imposes a capacity limit $j\le1$. Reading of the page: $i+j\le T$ is how §2's requirement $\max(0,k-n)\le T$ holds whatever the demand; $(i,0)\in A$ (producing nothing is possible) is implicit in §2.
• The terminal stock is computed by truncated subtraction in $\mathbb N$, which equals $\max(0,k-n)$. Sums over demands are tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.
• A statistical equilibrium is a stationary distribution of the chain of the rule, defined from the transition probabilities, not from (8). The expected monthly cost is defined from the joint law of (stock, production, demand), not as $\sum c_{ij}x_{ij}$. The LP constraint set omits (8.0), exactly as the page does.
• The decoded rule uses the default action $j=0$ at stock levels with $\sum_jx_{ij}=0$; any admissible default would do.
• Table 2's $x_{30}=\varepsilon$ is the paper's device against degeneracy; the example's solution has $x_{30}=0$. Footnote 5 prints no price for (4); $31/9$ is the price forced by equal objectives, and the dual optimum is not claimed unique.

Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as $\sum c_{ij}x_{ij}$ (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.

Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.

Selected references

• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3), 259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• H. M. Wagner, On the Optimality of Pure Strategies, Management Science 6(3), 268–269, 1960. https://doi.org/10.1287/mnsc.6.3.268
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• F. d'Epenoux, A Probabilistic Production and Inventory Problem, Management Science 10(1), 98–108, 1963 (translation of the 1960 French paper). https://doi.org/10.1287/mnsc.10.1.98

Why bias optimality matters

A finite Markov decision problem can have several policies with the same long-run average reward even though they behave differently before reaching a recurrent class. Average reward discards a finite initial advantage: dividing total reward by the horizon sends any fixed transient contribution to zero. In applications where the process runs for a long but unspecified time, this leaves a genuine choice among average-optimal policies. Bias optimality uses discounted values as the discount factor approaches one to resolve that choice. Kallenberg develops the criterion in Chapter 5 of Linear Programming and Finite Markovian Control Problems, following Blackwell's earlier notion of a nearly optimal policy.

The chapter asks for a way to recognize a bias optimal policy without comparing it directly with every possible sequence of history-dependent, randomized decisions. Its central characterization, Theorem 5.2.2, gives three tests involving only pure stationary policies. That change in the comparison class matters: there are finitely many pure stationary rules, while a general policy may depend on an unbounded history. The theorem also explains why average optimality alone leaves policies untied only at the gain level, while their bias vectors can differ. The two-state example in Figure 5.2.1 exhibits an average-optimal stationary rule that is not bias optimal (Kallenberg, pp. 163–164).

The finite decision model

The state space is $E=\{1,\ldots,N\}$ with $N>0$. Each state $i$ has its own finite, nonempty set $A(i)$ of admissible actions. Choosing $a\in A(i)$ earns the real reward $r_{ia}$ immediately and moves to state $j$ with probability $p_{iaj}$. The rows are stochastic: $p_{iaj}\ge0$ and $\sum_jp_{iaj}=1$. This is the chapter's standing assumption, stated at the opening of §5.2 (Kallenberg, p. 162).

A policy $R\in C$ assigns a probability distribution on the actions available at the current state after every finite history. Thus $C$ includes randomized and history-dependent decisions. A pure stationary policy $f^\infty\in C_D$ instead fixes one action $f(i)\in A(i)$ for each state and uses it in every period. Time starts at $t=1$. From initial state $i$, let $v_i^t(R)$ be expected reward in period $t$, and let $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}v_i^t(R)$ be expected discounted reward for $0\le\alpha<1$. The optimal discounted value $v_i^\alpha$ is the supremum of $v_i^\alpha(R)$ over all $R\in C$, taken separately for each state.

The average reward is $\phi_i(R)=\liminf_{T\to\infty}T^{-1}\sum_{t=1}^T v_i^t(R)$; its optimal value $\phi_i$ is again the statewise supremum over $C$. The corresponding limsup is $\hat\phi_i(R)$. A policy is average optimal when $\phi_i(R)=\phi_i$ at every state. It is bias optimal when $v_i^\alpha(R)-v_i^\alpha\to0$ as $\alpha\uparrow1$ at every state (Kallenberg, pp. 21–23 and 161).

For a pure stationary $f$, write $P(f)_{ij}=p_{i,f(i),j}$ and $r(f)_i=r_{i,f(i)}$. The stationary matrix $P^*(f)$ is the Cesàro limit of the powers of $P(f)$. The deviation matrix and bias vector are

$$D(f)=\bigl(I-P(f)+P^*(f)\bigr)^{-1}-P^*(f), \qquad u(f^\infty)=D(f)r(f).$$

The gain of $f^\infty$ is $\phi(f^\infty)=P^*(f)r(f)$. These are the book's Definitions 2.4.2 and notation (2.5.5), and their finite stochastic-matrix properties are recorded in Theorem 2.4.1 (Kallenberg, pp. 29 and 33–34).

Formalization targets

The goal is Theorem 5.2.2, for each pure stationary $f_*^\infty$. It asserts that the following are equivalent: (i) $f_*^\infty$ is bias optimal against the value over all $C$; (ii) for every $f^\infty\in C_D$, the vector limit $\lim_{\alpha\uparrow1}\bigl(v^\alpha(f_*^\infty)-v^\alpha(f^\infty)\bigr)$ exists and is nonnegative; (iii) $f_*^\infty$ is average optimal and, at every state $i$, its bias is maximal among pure stationary policies optimal at that state; and (iv) for every $f^\infty\in C_D$, the vector limit

$$\lim_{T\to\infty}\frac1T\sum_{t=1}^T\sum_{s=1}^t \bigl(v^s(f_*^\infty)-v^s(f^\infty)\bigr)\ge0$$

exists. These limits are read in the extended reals: a strictly positive gain gap makes a difference tend to $+\infty$, which satisfies the displayed inequality. The period rewards $v^s$ in the last formula are not discounted values. The printed clause (iii) has a typographical error in the set following max; its proof on p. 164 supplies the intended restriction $\phi_i(f^\infty)=\phi_i$. The formal statement uses that reading and records it explicitly.

Two earlier chapter results are milestones. Lemma 5.2.1 bounds the Abel limsup $(1-\alpha)v_i^\alpha(R)$ by the upper average reward $\hat\phi_i(R)$ for any policy. Theorem 5.2.1 says that bias optimality implies average optimality, with a two-state example showing that average optimality does not imply bias optimality. The later §5.3 linear-programming construction is a separate route to finding a bias optimal policy and is outside this mission's statement layer.

What the characterization gives

The equivalence allows bias optimality to be checked through discounted differences, bias vectors, or accumulated period rewards. Its bias-vector clause identifies the relevant comparison set: a policy can be optimal in average reward at one state without being optimal at every state, and that statewise distinction cannot be discarded. It also makes the bias criterion finer than average optimality, as the two-state counterexample shows (Kallenberg, pp. 163–165).

The source proves these results; the mission asks for machine-checked proofs of the stated equivalence and its two supporting results. The finite history and reward definitions can support later formalizations of Kallenberg's average-reward and constrained models. The matrix definitions can also be reused for results about finite Markov chains, including the Cesàro limit and deviation matrix. No machine-checked proof of this specific four-way characterization is claimed here.

Where the difficulty lies

Comparing average rewards alone loses the transient reward information that bias is designed to retain. The discounted comparison has an apparent divergence of order $(1-\alpha)^{-1}$ whenever two policies have different gains; the finite residual becomes meaningful only after those gain terms are separated. The accumulated-reward test also takes a second Cesàro average, so a direct identification with ordinary average reward would miss its bias contribution. The theorem has to preserve both the gain ordering and the finite bias remainder across these limiting regimes (Kallenberg, pp. 164–165).

For a general policy, the discounted value is defined by infinitely many history-dependent choices, whereas $P^*$ and $D$ apply to one fixed stationary matrix. This is the obstacle in passing from clause (i), which compares with all $C$, to the tests against $C_D$. Treating the optimal discounted value as a supremum over stationary policies by definition would erase that obstacle and change the theorem.

Formalization scope

Lean uses Fin N with $N>0$ for states and a finite action type with nonempty state-dependent admissible subsets. Rewards are real, transition rows are stochastic, and policies are distributions on actions after complete finite histories. The finite sum of products defining each history's probability supplies $v_i^t(R)$; no measure-theoretic path space is needed. Discounted rewards use a real infinite sum for $\alpha$ near one from below. Average rewards are real liminf and limsup values of bounded sequences. Optimal values are statewise suprema over all admissible policies, not over just $C_D$.

The matrix $P^*$ is a Cesàro limit and $D$ uses the book's inverse formula. Their convergence and nonsingularity for finite stochastic matrices are mathematical obligations, not added assumptions of the goal. The $T=0$ value of a totalized average and the value of a discounted sum outside its summable range do not enter the limits. Contributions to the finite-chain limit facts, boundedness of reward criteria, the Abel/Cesàro comparison, and the four equivalences are all within scope. A formalization that restricts the optimum in bias optimality to pure stationary policies would not be this theorem.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. Publisher repository.
• David Blackwell, “Discrete Dynamic Programming,” Annals of Mathematical Statistics 33 (1962), 719–726. DOI.