Linear Optimization

Motivation

Scheduling independent jobs on unrelated parallel machines to minimize the makespan is one of the basic NP-hard problems of scheduling theory: each job has its own processing time on each machine, with no relation between machines, and the goal is to finish all jobs as early as possible. When the number of machines is part of the input, Lenstra, Shmoys and Tardos showed that no polynomial algorithm can come within a factor below 3/2 of the optimum unless P = NP. When the number of machines $m$ is a fixed constant, the picture is different: the problem admits a polynomial approximation scheme, a family of algorithms that reach any accuracy $1+\varepsilon$.

Such a scheme was already known. Horowitz and Sahni (1976) gave a fully polynomial approximation scheme for fixed $m$, but its space requirement grows like $(nm/\varepsilon)^m$. The second application of the Rounding Theorem in the 1987 report of Lenstra, Shmoys and Tardos is a scheme whose space is polynomial in the input size, in $m$, and in $\log(1/\varepsilon)$. This mission formalizes the approximation guarantee of that scheme (Theorem 3 of the report).

Timeline:

• 1976. Horowitz and Sahni, a fully polynomial approximation scheme for a fixed number of unrelated machines, with exponential space in $m$.
• 1985. Potts, a 2-approximation for unrelated machines whose running time is $m^{m-1}$ times a polynomial, based on LP rounding with enumeration.
• 1987. Lenstra, Shmoys and Tardos, the Rounding Theorem, a polynomial 2-approximation for arbitrary $m$, and, for fixed $m$, the scheme formalized here (FOCS 1987; journal version in Mathematical Programming 46, 1990).

Setting

There are $m$ machines and $n$ jobs. If job $j$ is scheduled on machine $i$ it takes $p_{ij}$ time units, a positive integer; $P=(p_{ij})$ is the processing-time matrix. A schedule $\sigma$ assigns every job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} p_{ij}$, the makespan is the largest load, and $\mathrm{OPT}$ is the smallest makespan over all schedules.

Fix an integer deadline $d\ge0$ and an accuracy $\varepsilon>0$. Assigning job $j$ to machine $i$ is long if $p_{ij}>\varepsilon d$ and short otherwise. A schedule of long assignments $L$ is a partial assignment of jobs to machines using only long assignments; its long load on machine $i$ is $t_i$, and $L$ is admissible if $t_i\le d$ for every $i$.

For a threshold $t$ and deadlines $d_1,\dots,d_m$, the linear program (LP) of the Rounding Theorem has a variable $x_{ij}\ge0$ for every pair with $p_{ij}\le t$, the constraints $\sum_i x_{ij}=1$ for each job, and $\sum_j p_{ij}x_{ij}\le d_i$ for each machine. The residual LP of $(d,L)$ is (LP) for the jobs left unassigned by $L$, with $d_i=d-t_i$ and $t=\varepsilon d$.

The procedure $A_\varepsilon$, on input $d$, tries every admissible $L$; if the residual LP is feasible it takes a vertex $\tilde x$, rounds it to a 0-1 solution of the integer program (IP) of the Rounding Theorem, and combines the result with $L$. It answers 'no' if no residual LP is feasible. A $\rho$-relaxed decision procedure answers 'no' only when no schedule has makespan at most $d$, and otherwise returns a schedule of makespan at most $\rho d$. The binary search of Lemma 1 runs such a procedure on deadlines between $\lceil t/m\rceil$ and $t$, where $t$ is the makespan of the greedy schedule, and returns the best schedule found.

Formalization targets

Goal: Theorem 3

For every $m\ge1$, every positive integer matrix $P$, every $\varepsilon>0$, every LP solver $V$, the procedure $A_\varepsilon$ run with $V$ exists, and the binary search driven by any such procedure returns a schedule $\sigma$ with

$$\mathrm{makespan}(\sigma)\le(1+\varepsilon)\,\mathrm{OPT}.$$

Milestones (§3, p. 6)

1. Every machine in an admissible $L$ carries fewer than $1/\varepsilon$ long assignments, and for $n,m\ge1$

$$\#\{L\text{ admissible}\}<(n+1)^{m/\varepsilon}.$$

2. If some schedule has makespan at most $d$, its long part is admissible and its short part is a feasible solution of the residual LP.
3. If the short assignments take at most $d-t_i+\varepsilon d$ on machine $i$, the combined schedule has load at most $(1+\varepsilon)d$ on every machine.
4. $A_\varepsilon$ exists for every LP solver and is a $(1+\varepsilon)$-relaxed decision procedure.

Significance

Theorem 3 shows that for a fixed number of unrelated machines, the makespan can be approximated to any accuracy in polynomial time while keeping the memory polynomial in $\log(1/\varepsilon)$. It is an early instance of the pattern "enumerate the large items, solve an LP for the small ones, round", which recurs in later approximation schemes for scheduling and packing. Together with the 2-approximation of the same paper (mission 1 of this series) and the 3/2 hardness bound (mission 3), it delimits what is achievable for unrelated machines.

The theorem is proved in the paper; none of it is known to have a machine-checked proof. Formalizing it requires a precise account of the enumeration of long assignments, the residual LP, and the binary search, and it exercises the Rounding Theorem, which this series poses in mission 1, outside its original setting (with a non-integral threshold $t=\varepsilon d$).

Difficulty

The arithmetic of the scheme is short; the content lies in the Rounding Theorem, which turns a vertex of the residual LP into a 0-1 schedule exceeding each deadline by at most the threshold. The obvious argument, rounding an arbitrary feasible LP solution, fails: a non-vertex solution may split many jobs across many machines, and rounding them can overload a machine by far more than $t$. The bound depends on the structure of vertices of (LP), which an arbitrary feasible point does not have. A second difficulty is the count of milestone 1, which must be done with a real exponent $m/\varepsilon$ and a strict inequality.

Formalization scope

• Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive. Load, makespan and optimal schedules are those of the published MatousekLP.Scheduling.Schedule, applied to the real cast of P.
• A vertex of an LP is a point of Set.extremePoints of its feasible region. Variables absent from the paper's (LP) are kept as matrix entries fixed to $0$, which leaves the vertices unchanged.
• The LP solver is a parameter (a vertex selector) and $A_\varepsilon$ is a predicate on procedures: each answer must extend an admissible schedule of long assignments, round the selected vertex within its support, and satisfy the (IP) load bound. The guarantee is proved for every such procedure. The output is thereby tied to what the algorithm computes, so the bound is not witnessed by an optimal schedule.
• The binary search is a definition: greedy start, $l=\lceil t/m\rceil$ (the paper's $t/m$ rounded up because makespans are integers), $d=\lfloor(u+l)/2\rfloor$, best stored schedule as output.
• Not formalized: that $m$ is fixed, the polynomial running time, and the space bound polynomial in $m$, $\log(1/\varepsilon)$ and the input size. The guarantee is stated for every $m\ge1$. The count $(n+1)^{m/\varepsilon}$ of milestone 1, on which the running-time claim rests, is formalized, with the real power Real.rpow.
• The constants are exact: $1+\varepsilon$, $(n+1)^{m/\varepsilon}$, $d-t_i+\varepsilon d$. Milestone 1 needs $n\ge1$ and $m\ge1$ for strictness.
• Theorem 1 (the Rounding Theorem) and Lemma 1 are milestones of mission 1 of this series and are not restated here.

Welcome contributions: a proof of the Rounding Theorem in the generality of real deadlines and thresholds, proofs of the counting bound, and lemmas on the binary search that are reusable for any relaxed decision procedure.

Selected references

• J.K. Lenstra, D.B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source; Theorem 3, p. 6). Journal version: Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951
• C.N. Potts, Analysis of a linear programming heuristic for scheduling unrelated parallel machines, Discrete Applied Mathematics 10 (1985) 155–164. https://doi.org/10.1016/0166-218X(85)90009-5
• D.S. Hochbaum, D.B. Shmoys, Using dual approximation algorithms for scheduling problems: theoretical and practical results, Journal of the ACM 34 (1987) 144–162. https://doi.org/10.1145/7531.7535

Motivation

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).

Timeline:

• 1956–1963. Ford and Fulkerson prove max-flow = min-cut for one commodity; Hu (1963) proves equality for two commodities.
• 1981–1990. Okamura and Seymour give a 4-commodity example with max-flow 3/4 and min-cut 1. Schrijver (1990), combining Lomonosov and Papernov, characterizes demand graphs for which equality always holds. Shahrokhi and Matula (1990) prove equality for uniform demands under a condition on the dual.
• 1988. Leighton and Rao (FOCS 1988) prove the $\Theta(\log n)$ gap for uniform demands; the journal version (1999) is the source of this mission.
• 1995. Linial, London and Rabinovich, and independently Aumann and Rabani, extend the bound to arbitrary demands with $O(\log k)$ for $k$ commodities, via metric embeddings (Combinatorica 1995).

Setting

A network is a finite set $V$ of $n$ nodes with a capacity $C(u,v)=C(v,u)\ge0$ for every pair; the pair is an edge when $C(u,v)>0$. For $U\subseteq V$ with complement $\bar U$, the cut capacity $C(U,\bar U)$ is the total capacity of the edges joining $U$ to $\bar U$. As in the paper, the network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$.

In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value $\lambda$ sends $\lambda$ units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow $f$ is the largest such $\lambda$ (the concurrent max-flow).

The min-cut (sparsest cut) of the UMFP is

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

the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity $C(U,\bar U)/(|U||\bar U|)$ is the ratio cost of the cut.

The milestones use the dual objects. A distance function $d$ assigns a nonnegative length to each edge; $d(u,v)$ is then the shortest-path distance, $d(T,u)=\min_{t\in T}d(t,u)$, and the total weight is $W=\sum_{e}C(e)d(e)$. The distance constraint (5) is $\sum_{\{u,v\}}d(u,v)\ge1$, summed over unordered pairs. A set of nodes has radius at most $\Delta$ if some centre reaches all its nodes by walks inside the set of length at most $\Delta$. Throughout, $\log n=\log_2 n$.

Formalization targets

Goal: Theorem 2 (p. 795)

$$\Omega\!\left(\frac{\mathcal S}{\log n}\right)\le f\le\mathcal S$$

for every uniform multicommodity flow problem: there is one absolute constant $c>0$ such that $c\,\mathcal S/\log n\le f\le\mathcal S$ for every connected network with $n\ge2$ nodes. The goal fixes no constant, so it is the form any improved argument would still prove.

Milestones, in the order the argument uses them

1. Weak duality (§1.2, pp. 789–790): every concurrent flow of value $\lambda$ satisfies $\lambda\,|U||\bar U|\le C(U,\bar U)$ for every cut.
2. LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$, and some such function has $W=f$.
3. Lemma 3 (p. 797): for every $\Delta>0$, $V$ splits into components of radius at most $\Delta$ with at most $4W\log n/\Delta$ capacity between components.
4. Corollary 4 (pp. 798–799): either a set of at least $2n/3$ nodes has radius at most $1/(2n^2)$, or some cut has ratio cost at most $36W\log n$.
5. Lemma 5 (p. 799): if $|T|\ge 2n/3$ and $\sum_{u\notin T}d(T,u)\ge 1/(2n)$, some cut has ratio cost at most $6W$.
6. Lemma 6 (p. 800): a distance function satisfying (5) yields a cut of ratio cost at most $36W\log n$.

Companion

$\mathcal S\le 36\,f\log n$ and $f\le\mathcal S$: Theorem 2 with the constant its proof produces.

Significance

The theorem says that the LP relaxation of uniform sparsest cut has integrality gap $O(\log n)$, and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an $O(\log n)$-approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.

The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a $\log n$ factor against the total weight $W$, which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.

Formalization scope

• Nodes and capacities. V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form $C(U,\bar U)>0$ for every nonempty proper $U$ (the paper's standing assumption, p. 789).
• Demands and flows. Each unordered pair is encoded as two ordered commodities with demand $\tfrac12$ (the paper's footnote 2). Flows are arc flows with conservation per commodity, and both directions of an edge share its capacity. The max-flow is the real supremum of feasible values; with $n\ge2$ that set is nonempty and bounded.
• Cuts. The min-cut ranges over nonempty proper subsets only. Including $U=\emptyset$ or $U=V$ would give $0/0$, which Lean evaluates to $0$ and which would make the goal trivially true; this formalization excludes it.
• Distances. $d(u,v)$ is an infimum over walks in the graph, meaningful under connectivity; the radius of a component is measured by walks inside it.
• Constants. The goal keeps the page's $\Omega$ with a single universal constant chosen before the network. The milestones carry the constants computed in the paper's proofs ($36$ in Corollary 4 and Lemma 6, $6$ in Lemma 5), and each statement says so.
• Algorithms. "We can find" is formalized as existence. Running times and the remark that the proofs yield polynomial-time algorithms (p. 801) are out of scope.

Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing 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
• 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
• H. Okamura and P. D. Seymour, Multicommodity flows in planar graphs, J. Combin. Theory Ser. B 31:75–81, 1981. https://doi.org/10.1016/S0095-8956(81)80012-3
• 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
• V. Chvátal, Linear Programming, W. H. Freeman, 1983.

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$, and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$. The primal problem minimizes $c^Tx$ over $Ax=b$, $x\ge0$. Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$, $s\ge0$. The dual slack is $s$. The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$, with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$. For $0<\beta<1$, the Euclidean central-path neighborhood is

$$N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.$$

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$, $Ad_x=0$, and $A^Td_y+d_s=0$. A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$. Algorithm 1 begins in $N_2(1/4)$. It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$, then takes one full corrector direction with $\gamma=1$. The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$, every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

$$k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.$$

The paper states the iteration order as $O(\sqrt n\,t)$. The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$, rather than with $n$, in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$. The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$: Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$, because its printed lower bound on the predictor length fails at $n=1$.

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

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. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

Motivation

An integer program is a linear program whose variables must take integer values. Its linear relaxation can be solved efficiently, while the integer program itself is NP-hard in general, so a recurring question in integer programming is how much the optimal solution of the relaxation says about the integer optimum. Simple rounding of the fractional optimum does not answer it: examples show that the integer optimum need not lie within distance one of the LP optimum, even when the right-hand side is large.

R. E. Gomory's 1965 note in the Proceedings of the National Academy of Sciences (doi:10.1073/pnas.53.2.260) showed that, for right-hand sides lying deep inside the cone of an optimal LP basis, the integer program is solved exactly by the LP solution plus a correction computed in a finite abelian group. The resulting group relaxation (the "corner polyhedron" of Gomory's later work, Gomory 1969) underlies a large body of work on cutting planes, the master group problem, Gomory–Johnson functions and asymptotic integer programming.

Timeline. Gomory's fractional cutting-plane algorithm (Gomory 1958) introduced the "fractional rows" of the simplex tableau; the 1965 note identifies the group they generate with $M(I)/M(B)$ and proves the asymptotic theorem formalized here. Gomory 1969 develops the corner polyhedron; Gomory and Johnson (1972) study the continuous valid functions of the corner polyhedron.

Setting

Let $A$ be an integer $m\times(m+n)$ matrix of the form $(A',I)$, let $b\in\mathbb Z^m$ and $c\in\mathbb R^{m+n}$. Problem P1 is

$$\max\ z_1=cx\quad\text{s.t.}\quad Ax=b,\ x\ge0,$$

and P2 is P1 with $x$ integer. A basis is a nonsingular $m\times m$ submatrix $B$ of $A$; after rearranging, $A=(B,N)$ with $B=(\alpha_1,\dots,\alpha_m)$ and $N=(\alpha_{m+1},\dots,\alpha_{m+n})$, and $c=(c_B,c_N)$. The relative cost of a nonbasic column is $c^*_i=c_i-c_BB^{-1}\alpha_i$, and $B$ is an optimal basis when all $c^*_i\le0$. The cone of the basis is $K^B=\{\beta\in\mathbb R^m: B^{-1}\beta\ge0\}$; removing from it all points within Euclidean distance $d$ of its boundary gives the reduced cone $K^B(d)$.

Let $M(I)=\mathbb Z^m$ and $M(B)=\mathfrak L_B$ the lattice of integer combinations of $\alpha_1,\dots,\alpha_m$. The factor module $M(I)/M(B)$ is a finite abelian group with $D=|\det B|$ elements; write $\bar\alpha_i$, $\bar b$ for the classes of $\alpha_i$, $b$. The group problem (4) is

$$\max\ \sum_{i=1}^n c^*_{i+m}y_i\quad\text{s.t.}\quad\sum_{i=1}^n\bar\alpha_{i+m}y_i=\bar b,\quad y_i\ge0\text{ integer},$$

with optimal value $\varphi^B(b)$. Finally $l=\max_{i>m}\|\alpha_i\|$.

Formalization targets

Goal: THEOREM 1 (p. 261)

If $b\in K^B(l(D-1))$, then P1, P2 and (4) attain their optima, the value $z_2(b)$ of P2 is

$$z_2(b)=z_1(b)+\varphi^B(b),$$

an optimal solution of P2 is

$$x(b)=\big(B^{-1}(b-Ny^B(b)),\ y^B(b)\big)$$

for an optimal solution $y^B(b)$ of (4) with $\sum_iy^B_i(b)\le D-1$, and $\varphi^B$, $y^B$ are $m$-periodic: $\varphi^B(b+\alpha_i)=\varphi^B(b)$.

Milestones

In the order of the paper's proof: $|M(I)/M(B)|=D$ (p. 262); periodicity of (4) (p. 263); the cost identity (5)–(6); "$c_BB^{-1}b$ is $z_1(b)$", the simplex optimality criterion (a published, proved theorem); the projection of a solution of P2 to a solution of (4); the bound (7), $z_2(b)\le z_1(b)+\varphi(b)$; the extension of a solution of (4) to an integer solution; the LEMMA (an optimal solution of (4) with $\sum y_i\le D-1$); and the bound $\|Ny\|\le(D-1)l$ that places $b-Ny$ in $K^B$.

Companions

THEOREM 2: the optimal $x(b)$ satisfies $\sum_{i>m}x_i=\sum_iy_i\le D-1$. THEOREM 4 (with the bound corrected, see below): if an optimal $y$ of (4) has $\prod_i(y_i+1)>D$, the optimum of (4) is not unique.

Significance

THEOREM 1 reduces integer programming, for right-hand sides far from the boundary of an optimal cone, to a shortest-path-type problem over a group of order $D$: the integer optimum is determined by the LP optimum and a periodic correction, and it can be computed in time polynomial in $n$ and $D$ (THEOREM 3, not formalized here). It explains why rounding fails while a structured correction succeeds, and it is the starting point of the corner-polyhedron and cutting-plane theory built on the group relaxation. THEOREM 2 bounds how far the integer optimum lies from a lattice point of $\mathfrak L_B$, an early proximity result.

The results are classical and proved in the paper; none of them has a machine-checked proof that this mission is aware of. The mission produces a Lean statement and proof of the asymptotic theorem, together with reusable statements about the group $\mathbb Z^m/B\mathbb Z^m$ and the zero-sum shortening argument of the LEMMA.

Difficulty

The decomposition $z_2\le z_1+\varphi$ is a direct computation. The difficulty is the converse: an optimal solution $y$ of the group problem extends to an integer point $x_B=B^{-1}(b-Ny)$, but nothing in (4) forces $x_B\ge0$. Optimality of $y$ alone does not bound $y$: an optimal solution may carry zero-cost cycles of arbitrary length, and then $b-Ny$ can leave the cone $K^B$. The theorem therefore depends on choosing the right optimal solution of (4), one whose total size is bounded by the group order, and on relating that combinatorial bound to the Euclidean geometry of the cone.

Formalization scope

• The basis is fixed: $B$ is an integer $m\times m$ matrix and $N$ an integer $m\times n$ matrix; column $j$ of $N$ ($0$-based) is the paper's $\alpha_{m+1+j}$. The costs $c_B$, $c_N$ are real.
• The standing assumptions of pp. 260–262 are hypotheses of the goal: $\det B\neq0$; every unit vector of $\mathbb Z^m$ is a column of $B$ or of $N$ (the paper's $A=(A',I)$, without which P2 can be infeasible); all relative costs $c^*_i\le0$ ($B$ is optimal, without which (4) is unbounded).
• P2's variables are natural numbers (integer and nonnegative). The group problem is written as "$b-Ny\in B\mathbb Z^m$", which is equivalent to $\sum\bar\alpha_{i+m}y_i=\bar b$.
• Optimal values are greatest elements of the sets of objective values, never suprema; the goal asserts that they are attained.
• The norm in $l$ and in $K^B(d)$ is Euclidean. $K^B(d)$ is the set of points whose closed ball of radius $d$ lies in $K^B$. $l=0$ when $n=0$.
• In part (3) of the goal, $y^B(b)$ ranges over optimal solutions of (4) with $\sum_iy_i\le D-1$, the solutions the paper's LEMMA and dynamic program produce.
• THEOREM 4 is stated with the hypothesis $\prod(y_i+1)>D$: the printed $>D-1$ is false ($m=n=1$, $B=(2)$, $N=(1)$, $c=(2,0)$, $b=1$ has the unique optimum $y=1$ with $\prod(y_i+1)=2$).
• A trivializing formalization is ruled out: the goal assumes none of the LEMMA, the inequality (7), integrality of $B^{-1}(b-Ny)$ or the norm bound, and it states the existence of the optima instead of assuming them.
• Not in scope: the operation counts of THEOREM 3 and the recursion (8), which need a machine model the paper does not define.

Needed infrastructure: the cardinality of $\mathbb Z^m/B\mathbb Z^m$ (available in Mathlib through determinants of basis changes), a zero-sum/pigeonhole argument in a finite abelian group, the simplex optimality criterion (published), and elementary Euclidean estimates. The group-theoretic lemmas are reusable for other group-relaxation and proximity missions. Proofs of the milestones, alternative arguments and the extension to the open-ball reading of $K^B(d)$ are welcome.

Selected references

• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proc. Natl. Acad. Sci. USA 53(2):260–265, 1965. https://doi.org/10.1073/pnas.53.2.260
• R. E. Gomory, Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc. 64:275–278, 1958. https://doi.org/10.1090/S0002-9904-1958-10224-4
• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra Appl. 2:451–558, 1969. https://doi.org/10.1016/0024-3795(69)90017-2
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Math. Programming 3:23–85, 1972.
• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer, 2007 (simplex optimality criterion). https://doi.org/10.1007/978-3-540-30717-4

Motivation

The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.

In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.

Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.

Setting

A network has finitely many nodes $P_1,\dots,P_N$ and arcs $A_1,\dots,A_m$. Each arc $A_r$ joins two nodes, has a capacity $b_r$, and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity $k$ has a set of sources $S_k$ and a set of sinks $T_k$.

A chain from $u$ to $w$ is the arc set of a path $u = v_0, v_1, \dots, v_p = w$ with distinct nodes, each arc traversable from $v_{i-1}$ to $v_i$. A commodity chain of $k$ is a chain from a node of $S_k$ to a node of $T_k$. List the commodity chains, for all commodities, as $C_1,\dots,C_n$, and let $A = (a_{rs})$ be the incidence matrix: $a_{rs} = 1$ if $C_s$ contains $A_r$ and $0$ otherwise. With $x_s$ the flow along $C_s$ and $x_{n+r}$ the slack of arc $A_r$, the problem is the linear program

$$\text{maximize } \sum_{s=1}^{n} x_s \quad\text{subject to}\quad \sum_{s=1}^{n} a_{rs}x_s + x_{n+r} = b_r,\qquad x_1,\dots,x_{n+m} \ge 0. \tag{2–3}$$

A basis is a set of $m$ columns of $[A \mid I]$ forming an invertible matrix $B = (b_{rj})$. Its simplex multipliers $\alpha_1,\dots,\alpha_m$ satisfy, for every basic column $j$,

$$\sum_{r=1}^{m} \alpha_r b_{rj} = \begin{cases} 1 & j \le n,\\ 0 & j > n.\end{cases} \tag{4}$$

Read as arc lengths, the $\alpha_r$ give each chain $C_s$ the length $\sum_r \alpha_r a_{rs}$. The labeling process for a source set $S$ starts with labels $\pi_i = 0$ on $S$ and $\pi_i = \infty$ elsewhere. It repeatedly finds an arc traversable from $P_i$ to $P_j$ with $\pi_i + l_{ij} < \pi_j$ and replaces $\pi_j$ by $\pi_i + l_{ij}$. In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.

Formalization targets

Goal: the shortest-chain pricing test (§3, pp. 1779–1780)

Let $B$ be a basis with basic feasible solution $z$ and multipliers $\alpha \ge 0$. Then:

$$\begin{aligned} &\text{(a) for every commodity, every run of the labeling process with lengths } \alpha \text{ is finite;}\\ &\text{(b) if all final sink labels are } \ge 1, \text{ then } \textstyle\sum_s x_s \le \sum_s z_s \text{ for every feasible } x;\\ &\text{(c) if a final sink label } \pi_t < 1, \text{ some non-basic chain column to } t \text{ has length } \pi_t \text{ and } 1 - \textstyle\sum_r \alpha_r a_{rs} > 0. \end{aligned}$$

Milestones (§3, the labeling process and the test)

1. Termination of the labeling process for non-negative lengths (p. 1780).
2. Final labels are shortest-chain lengths from $S$; the smallest label on $T$ is the $S$-to-$T$ distance (p. 1780).
3. The trace-back: a chain of tight arcs from $S$ to every labeled node, of length its label (p. 1780).
4. If $\alpha \ge 0$ and every commodity chain has length $\ge 1$, the basis is optimal (p. 1779).

Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.

Significance

The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the $m \times m$ basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.

Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches $S$ only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.

Difficulty

The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often $0$) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from $S$), and it is terminal. A terminal labeling alone, such as all labels $0$, is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), $\alpha \ge 0$ and the shortest-chain lengths, with the chain columns indexed abstractly.

Formalization scope

Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance $0$. Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of $[A \mid I]$ are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for $\infty$. Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case $l_{ij} = l_{ji}$.

The standing assumption of §3 ("a stage has been reached in the computation where all $\alpha_r$ are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.

A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.

Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.

Selected references

• L. R. Ford Jr., D. R. Fulkerson, A suggested computation for maximal multi-commodity network flows, Management Science 5(1):97–101, 1958; reprinted Management Science 50(12S):1778–1780, 2004. https://doi.org/10.1287/mnsc.1040.0269
• L. R. Ford Jr., D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
• L. R. Ford Jr., Network Flow Theory, RAND Corporation Paper P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• G. B. Dantzig, P. Wolfe, Decomposition principle for linear programs, Operations Research 8(1):101–111, 1960. https://doi.org/10.1287/opre.8.1.101
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007. https://doi.org/10.1007/978-3-540-30717-4

Why minimum-cost circulation needs a real-cost iteration bound

A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.

This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.

Network and approximate optimality

The vertex set $V$ is finite, with $n=|V|$, and $E$ is a symmetric set of directed arcs, with $m=|E|$. Symmetry means that $(v,w)\in E$ brings $(w,v)\in E$ too. Each arc has a real capacity $u(v,w)$ and a real cost $c(v,w)$; costs obey $c(v,w)=-c(w,v)$. A circulation $f$ obeys $f(v,w)\le u(v,w)$, $f(v,w)=-f(w,v)$, and conservation of flow at every vertex. Its total cost is half the sum of $c(v,w)f(v,w)$ over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.

The residual capacity is $u_f(v,w)=u(v,w)-f(v,w)$. For a price function $p:V\to\mathbb R$, the report writes the reduced cost as $c_p(v,w)=c(v,w)-p(v)+p(w)$. A circulation is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. It is $\varepsilon$-optimal if some price function works, where $\varepsilon\ge0$. The tight error $\varepsilon(f)$ is the least such error. A circulation is $\varepsilon$-tight when it is $\varepsilon$-optimal but fails to be $\varepsilon'$-optimal at every $\varepsilon'<\varepsilon$. This includes attainment at $\varepsilon$.

An arc is $\varepsilon$-fixed if all $\varepsilon$-optimal circulations carry the same flow through it. Write $F_\varepsilon$ for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of $2n$, $F_\varepsilon$ becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.

Formalization targets

The goal is the circulation-level form of Theorem 4.5. Begin with a circulation $f_0$ and a sequence $f_0,f_1,\ldots$ whose positive-error steps satisfy the contract of Figure 3: if $\varepsilon(f_k)>0$, the next circulation is $\varepsilon(f_k)/2$-optimal. With the report's standing $n\ge2$ and $m\ge n-1$, the target is

$$\exists k\le m\left\lceil\log_2(2n)\right\rceil:\quad \varepsilon(f_k)=0\quad\text{and}\quad f_k\text{ is minimum-cost}.$$

The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as $O(m\log n)$ iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.

What the result establishes

The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on $1/n$. The bound counts refinement calls only; the report analyzes the work within particular implementations separately.

The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.

Why the bound needs more than repeated halving

Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary $\varepsilon=0$, the printed wording of Lemma 4.4 would require $F_0$ to be a proper subset of itself, so its positive-error regime must be made explicit.

Formalization scope

The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes $m\ge n-1\ge1$ on printed page 5; the theorem binders express it as $n\ge2$ and $m\ge n-1$. The arc count is for ordered arcs, exactly as the report defines $m$. No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.

The reused 1989 definitions write reduced cost as $c(v,w)+p(v)-p(w)$. Substituting $-p$ for $p$ gives the report's $c(v,w)-p(v)+p(w)$, so existential price certificates, $\varepsilon$-optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set $F_\varepsilon$ is filtered from $E$ and includes only arcs whose flow is shared by all $\varepsilon$-optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.

The explicit reading of the report's asymptotic count is $t=\lceil\log_2(2n)\rceil$ halvings per factor-$2n$ reduction and at most $m$ such blocks, giving $m t$ refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.

Selected references

• A. V. Goldberg and R. E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987; journal version in Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI: 10.1287/moor.15.3.430. The mission's page and theorem indices refer to the 1987 report.

Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$: gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow the linear model

$$y = X\beta + z,$$

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$, each of Euclidean norm $\|X_j\|_{\ell_2}=1$; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$. Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$.

For a tuning level $\lambda_p>0$, a Dantzig selector $\hat\beta$ is any solution of

$$\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .$$

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$: the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$, $a\ge0$, and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$. If $\beta$ is $S$-sparse and $\delta_{2S}+\theta_{S,2S}<1-t$, then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),$$

with the explicit constant (1.14)

$$C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.$$

Milestones

1. Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$.
2. Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$, a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$, with bounds (6.1)–(6.6).
3. Corollary A.2 ($\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$.
4. Corollary A.3 (constrained thresholding): an $S$-sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$.
5. Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
6. Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$.

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$, uniformly over $S$-sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$-penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$, though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$. The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$), which forces $p\ge3$ and $\log p>0$. A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$, $\theta_{S,2S}$ of $X$, not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$, the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$. Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$. The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$, existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
• D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425

Motivation

Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.

In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has $2^{\Omega(\sqrt n)}$ inequalities.

Timeline.

• 1990: De Simone shows that the correlation polytope is linearly isomorphic to the cut polytope.
• 1991: Yannakakis proves the factorization theorem (extension complexity equals the nonnegative rank of a slack matrix) and the exponential lower bound for symmetric formulations of the TSP and perfect matching polytopes.
• 1992: Razborov proves the distributional lower bound for set disjointness.
• 2003: de Wolf shows that the support of $M(n)_{ab}=(1-a^\top b)^2$ needs $2^{\Omega(n)}$ rectangles to cover.
• 2012/2015: Fiorini et al. prove $\mathrm{xc}(\mathrm{CUT}(n))=2^{\Omega(n)}$, $\mathrm{xc}(\mathrm{TSP}(n))=2^{\Omega(\sqrt n)}$, and a $2^{\Omega(\sqrt n)}$ bound for stable set polytopes of some graphs on $n$ vertices.
• 2013: Kaibel and Weltge give a short combinatorial proof of the correlation-polytope bound, with constant $C=\log_2(3/2)$.
• 2014: Rothvoss proves $2^{\Omega(n)}$ for the perfect matching polytope.

Setting

Let $\iota$ be a finite index set. An extended formulation (EF) of a set $P\subseteq\mathbb R^{\iota}$ is a linear system $E^{=}x+F^{=}y=g^{=}$, $E^{\le}x+F^{\le}y\le g^{\le}$ in variables $(x,y)\in\mathbb R^{\iota}\times\mathbb R^{k}$ such that $x\in P$ exactly when some $y$ satisfies it. Its size is the number of inequalities. The extension complexity $\mathrm{xc}(P)$ is the least size of an EF of $P$.

A polytope is the convex hull of finitely many points. A face of $P$ is $P$ itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope $Q$ is an extension of $P$ if $\pi(Q)=P$ for some linear map $\pi$. Given $P=\{x : Ax\le b\}=\mathrm{conv}(V)$, the slack matrix has entries $S_{ij}=b_i-A_iv_j$. The nonnegative rank $\mathrm{rank}_+(M)$ is the least $r$ with $M=TU$, where $T\ge 0$ has $r$ columns and $U\ge 0$ has $r$ rows.

For $n$-bit strings $a,b$, $a^\top b$ is the number of common ones, and $M(n)$ is the $2^n\times 2^n$ matrix $M_{ab}=(1-a^\top b)^2$. A 1-monochromatic rectangle cover of its support is a family of products $R_1\times R_2$, each containing only entries with $M_{ab}\ne 0$, that together contain all of them.

On the complete graph $K_n=(V_n,E_n)$, $\chi^F\in\mathbb R^{E_n}$ is the characteristic vector of an edge set $F$ and $\delta(X)$ is the cut of $X\subseteq V_n$. The polytopes are

$$\mathrm{CUT}(n)=\mathrm{conv}\{\chi^{\delta(X)}\},\qquad \mathrm{COR}(n)=\mathrm{conv}\{bb^\top : b\in\{0,1\}^n\}\subseteq\mathbb R^{n\times n},$$ $$\mathrm{TSP}(n)=\mathrm{conv}\{\chi^F : F\subseteq E_n \text{ is a tour (Hamiltonian cycle) of } K_n\}.$$

Formalization targets

Goal: Theorem 12

$$\exists\,C>0\ \exists\,N\ \forall n\ge N:\qquad \mathrm{xc}(\mathrm{TSP}(n))\ \ge\ 2^{C\sqrt n}.$$

The constant is left unfixed, so the goal survives any improvement of it.

Milestones, in attack order

• Razborov's distributional bound (displayed in the proof of Theorem 1) and Theorem 1: every 1-rectangle cover of the support of $M(n)$ has $2^{\Omega(n)}$ rectangles.
• Lemma 2 and Theorem 3 (Yannakakis): $\mathrm{rank}_+(S)\le r$ $\iff$ an extension with at most $r$ facets $\iff$ an EF with at most $r$ inequalities.
• Theorem 4: $\mathrm{rank}_+(M)$ is at least the rectangle covering bound of its support (already proved on the platform, referenced).
• Theorem 5: $\mathrm{COR}(n)$ is linearly isomorphic to $\mathrm{CUT}(n+1)$. Lemma 6: $\langle 2\,\mathrm{diag}(a)-aa^\top,x\rangle\le 1$ is valid for $\mathrm{COR}(n)$, with slack $M_{ab}$ at $bb^\top$.
• Theorem 7: $\mathrm{xc}(\mathrm{CUT}(n+1))=\mathrm{xc}(\mathrm{COR}(n))\ge 2^{Cn}$.
• Lemma 9: $\mathrm{xc}$ does not increase under taking faces or linear images. Lemma 11: $\mathrm{TSP}(q)$ with $q=O(n^2)$ has a face that is an extension of $\mathrm{COR}(n)$.
• Stable sets: Lemma 8 and Theorem 10, $\mathrm{xc}(\mathrm{STAB}(G_n))=2^{\Omega(\sqrt n)}$ for some graph $G_n$ on $n$ vertices.

Significance

The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.

Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.

Difficulty

The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because $M(n)$ has rank $O(n^2)$. The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of $\mathrm{TSP}(q)$ with $q=O(n^2)$. Theorem 12 also needs a monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ that the paper only indicates.

Formalization scope

• Everything is over $\mathbb R$. Points of $\mathbb R^d$ are functions $\iota\to\mathbb R$ on a finite type. $\mathbb R^{E_n}$ has one coordinate per unordered edge of $K_n$ (non-diagonal elements of Sym2 (Fin n)). $\mathbb R^{n\times n}$ is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.
• $\mathrm{xc}$ and $\mathrm{rank}_+$ are natural numbers (sInf of the attainable sizes), never $\infty$, so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.
• Every $2^{\Omega(f(n))}$ is $\exists C>0\,\exists N\,\forall n\ge N$, $2^{Cf(n)}\le\cdot$ (real power). Every $O(n^2)$ is a constant $c$ with $\le c\,n^2$, uniform in $n$.
• Theorem 7 and Lemma 11 carry an added $n\ge 1$: at $n=0$ the printed statements fail, since $\mathrm{COR}(0)$ is a point with $\mathrm{xc}=0$ and no positive $q\le c\cdot 0$ exists.
• "Linearly isomorphic" in Theorem 5 is an injective linear map carrying $\mathrm{CUT}(n+1)$ onto $\mathrm{COR}(n)$, because the two ambient spaces have different dimensions.
• In Theorem 3, $\dim P\ge 1$ is "$P$ has two distinct points". Faces include $\emptyset$ and $P$, facets are maximal proper faces, and facets are counted with an explicit finite family.
• Ruled out: a TSP polytope over ordered pairs, all cycles or directed tours, a weakened isomorphism in Theorem 5, and an extension complexity valued in $\mathbb N\cup\{\infty\}$ that is infinite on a broken EF definition.
• Welcome contributions: proofs of any milestone, in particular Lemma 2 and the factorization theorem (reusable for every later extension-complexity result), Theorem 5, and the face construction of Lemma 11; a proof of the monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ as a supporting lemma.

Selected references

• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, J. ACM 62(2), Art. 17, 2015. https://doi.org/10.1145/2716307
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. Syst. Sci. 43(3), 441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• A. A. Razborov, On the distributional complexity of disjointness, Theoret. Comput. Sci. 106(2), 385–390, 1992. https://doi.org/10.1016/0304-3975(92)90260-M
• R. de Wolf, Nondeterministic quantum query and communication complexities, SIAM J. Comput. 32(3), 681–699, 2003. https://doi.org/10.1137/S0097539702407345
• C. De Simone, The cut polytope and the Boolean quadric polytope, Discrete Math. 79(1), 71–75, 1990. https://doi.org/10.1016/0012-365X(90)90056-N
• V. Kaibel, S. Weltge, A short proof that the extension complexity of the correlation polytope grows exponentially, Discrete Comput. Geom. 53, 397–401, 2015. https://doi.org/10.1007/s00454-014-9655-9
• T. Rothvoss, The matching polytope has exponential extension complexity, J. ACM 64(6), Art. 41, 2017. https://doi.org/10.1145/3127497