Linear Optimization

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$. Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ($L_\infty$) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$.

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

• 1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$.
• 1984. Megiddo extends the method to every fixed $d$, with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
• 1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$. Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
• 1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$. An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$, and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$. Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$. It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$, then $A$ row by row, then $b$. A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$, answers whether $a^Tx^*<b$, $=b$ or $>b$. Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$, the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

$$\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.$$

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

1. One query settles half of $n$ hyperplanes on the line ($A(1)=1$, $B(1)=\tfrac12$).
2. $v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$, so there is a basis in which all $a_{ij}\ne0$.
3. For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$, $H_k$.
4. A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$, and the middle hyperplane settles one of them.
5. Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
6. $C(d)\log n$ queries settle all $n$ hyperplanes.
7. If a hyperplane contains no optimal point, all optimal points lie on one side of it.
8. The oracle, Case I: at an optimum relative to $\{x_d=0\}$, two auxiliary systems decide the side or certify global optimality.
9. The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$, systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$, so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$, including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$. The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$, when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

• Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
• Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$. The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$. The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
• Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
• Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$. A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
• Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
• Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$, where the page's last sentence says $\{x_d<0\}$. The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$, the hypothesis its argument uses, since linear independence alone does not give it.
• Not included. Approach II and its bound $O(n(\log n)^{d^2})$, the remarks on slowly growing $d$, the randomized variants, and the applications of §1.
• Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
• N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
• M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
• K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
• R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
• B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

Motivation

The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in $n$ and $d$?

Timeline

• 1957. Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in Linear Programming and Extensions (1963).
• 1964–1966. Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
• 1967. Klee and Walkup (Acta Math.) refute the unbounded-polyhedron version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the $d$-step conjecture ($n = 2d$).
• 1970. Larman (Proc. LMS) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
• 1989. Naddef (Math. Programming) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$.
• 1992. Kalai and Kleitman (Bull. AMS) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
• 2010. Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches Polymath 3 on the polynomial version.
• 2010–2012. Santos (Annals of Math.) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width.
• 2014–2019. Todd (SIAM J. Discrete Math.) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel (Proc. LMS 2015) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial.

Setting

Work in $\mathbb{R}^d$. An H-polytope is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is

$$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$

where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.

A vertex of $P$ is an extreme point. Two vertices $u \ne v$ are adjacent when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an edge. The combinatorial diameter of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.

Formalization targets

Goal — the polynomial Hirsch conjecture

$$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$

Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.

Milestones — the known ladder

Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$.

Significance

A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.

None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.

Difficulty

The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.

Formalization scope

The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.

Welcome contributions: any milestone in any order (dimension_three_bound for $d \le 1$ cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.

Selected references

• V. Klee, D. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967). doi:10.1007/BF02392971
• D. Larman, Paths on polytopes, Proc. London Math. Soc. 20 (1970). doi:10.1112/plms/s3-20.2.249
• D. Naddef, The Hirsch conjecture is true for (0,1)-polytopes, Math. Programming 45 (1989). doi:10.1007/BF01589418
• G. Kalai, D. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. AMS 26 (1992). arXiv:math/9204233
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012). arXiv:1006.2814
• M. Todd, An improved Kalai–Kleitman bound for the diameter of a polyhedron, SIAM J. Discrete Math. 28 (2014). arXiv:1402.3579
• B. Matschke, F. Santos, C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015). arXiv:1202.4701
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010). doi:10.1287/moor.1100.0470
• F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013) (survey). arXiv:1307.5900

Linear programming for Markov decision problems

A Markov decision problem asks how to control a system that moves at random between finitely many states, where each decision changes the probabilities of the next move and incurs a cost. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) treats two criteria: the long-run average cost per period, and the total cost of driving the system into an absorbing state. Its Theorem 2 shows that, once attention is restricted to stationary procedures, each problem can be solved as a linear program over the state-action frequencies of the procedure. This mission formalizes that theorem, its supporting displays (3)–(10) and its Lemma on linear-fractional programs.

The linear programming formulation is now the standard computational and theoretical tool for constrained Markov decision processes, and its variables, the occupation measures, are the objects of most later work on that topic. Derman's paper is among the first to state it for the average-cost criterion. Manne (Linear Programming and Sequential Decisions, Management Science, 1960) gave an earlier average-cost formulation for an inventory model. The reduction of a ratio of linear functions to a linear program in Derman's Lemma is the transformation published in the same year by Charnes and Cooper (Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly, 1962).

Setting

There are finitely many states $0, \dots, L$ and decisions $d_1, \dots, d_K$, all available in every state. Making decision $d_k$ in state $i$ sends the system to state $j$ with probability $q_{ij}(k) \ge 0$, where $\sum_j q_{ij}(k) = 1$, and costs $w_{ik}$.

A procedure of class $C'$ is stationary randomized: in state $i$ it makes decision $d_k$ with probability $D_{ik}$, where $D_{ik} \ge 0$ and $\sum_k D_{ik} = 1$, independently of the past and of the time. Under such a procedure the states form a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$. Write $W_t$ for the expected cost at time $t$ when $X_0 = i$.

• Problem 1 (average cost): minimize $Q_R(i) = \limsup_{T\to\infty} \frac{1}{T}\sum_{t=0}^{T} W_t$. Here $w_{ik} > 0$, and Assumption A says that under every procedure of $C'$ all states belong to one class.
• Problem 2 (total cost): the state $L$ is absorbing under every decision and $w_{Lk} = 0$. Minimize $S_R(i) = \sum_{t=0}^{\infty} W_t$, the expected cost of reaching $L$. Assumption B says that under every procedure of $C'$, $L$ is reached from every state with probability one.

The state-action frequencies of a procedure $D \in C'$ with stationary distribution $\pi$ are $x_{jk} = \pi_j D_{jk}$. They satisfy the linear constraints

$$\text{(10)}\qquad x_{jk} \ge 0,\qquad \sum_k x_{jk} - \sum_{i}\sum_k x_{ik}\, q_{ij}(k) = 0 \ \ (j),\qquad \sum_j\sum_k x_{jk} = 1 .$$

For Problem 2, Derman adjoins a state $-1$ that restarts the chain uniformly on $0, \dots, L$ and is entered from $L$. The expected total cost then becomes a ratio of two linear functions of the frequencies of this augmented chain, (9).

Formalization targets

Goal: Theorem 2, pinned-down reading

The printed statement, "If Assumption A (B) holds, then problem 1 (2) can be formulated as a linear programming problem", is not a mathematical statement as it stands. The goal is the reading established by its proof (pp. 20–23).

Under Assumption A with $w > 0$, the program

$$\min \ \sum_{j,k} x_{jk} w_{jk} \quad \text{subject to (10)}$$

has an optimal solution. For every optimal $x^*$, every row sum $\sum_k x^*_{jk}$ is positive, and $D^*_{jk} = x^*_{jk}/\sum_k x^*_{jk}$ satisfies $Q_{D^*}(i) \le Q_D(i)$ for all $D \in C'$ and all $i$.

Under Assumption B with the Problem 2 costs, the linear program obtained from (9) by the Lemma's transformation, $\min \sum w_{jk} z_{jk}$ subject to (12), has an optimal solution. For every optimal $(z^*, z^*_{n+1})$ one has $z^*_{n+1} > 0$, and the procedure decoded from $x^* = z^*/z^*_{n+1}$ satisfies $S_{D^*}(i) \le S_D(i)$ for all $D \in C'$ and all $i$.

Milestones

In the order the proof uses them: the Cesàro limit and the unique positive stationary distribution of a one-class chain ((3), (5)); the taboo-probability identity (4); the formula (6) for $Q_R$; the cycle formula (7) for the averaged total cost; the remark that minimizing the average of the $S_R(i)$ minimizes each one; the correspondence between $C'$ and the solutions of (10); and the Lemma reducing a linear-fractional program under conditions (i) and (ii) to the linear program (12).

Significance

The theorem replaces a search over infinitely many randomized procedures by a single finite linear program. It also yields the structural fact that an optimal stationary procedure can be read off from any optimal solution. The variables $x_{jk}$ make constraints on long-run frequencies of actions expressible as linear constraints. That is the origin of the theory of constrained Markov decision processes, and of the dual linear programs whose variables are value functions. The Lemma is the classical linear-fractional reduction, used well beyond this setting.

All of these results are proved in the paper and in later textbooks (for example Puterman, Markov Decision Processes, 1994, §8.8 and §9.5). None of them has been formalized: Mathlib has Perron–Frobenius-type facts for irreducible matrices but no linear programming theory, no taboo probabilities and no Markov decision model. The mission produces machine-checked versions of the proof's chain of equalities and of the decoding step, written so that they can be reused for occupation-measure arguments.

Difficulty

Several steps fail in the naive argument. The correspondence between procedures and solutions of (10) needs every row sum $\sum_k x_{jk}$ to be positive. That uses Assumption A for a procedure obtained by completing the decoded rows arbitrarily, together with the uniqueness and positivity of the stationary distribution. Positivity of the stationary vector of an irreducible but possibly periodic chain, and the Cesàro (not ordinary) convergence of $P^t$, have no ready-made form in Mathlib. The total-cost identity (7) needs the regenerative identity (4), whose sums must first be shown to converge, and needs the augmented chain to be irreducible, which follows from Assumption B but is not assumed. Problem 2 needs one more step: a minimizer of the averaged total cost is optimal from every starting state, which uses the finiteness of all $S_R(i)$.

Formalization scope

States and decisions are finite Lean types S and Act. Probabilities and costs are real numbers, a procedure of $C'$ is a nonnegative real matrix with unit row sums, and the chain is chainMatrix q D. Assumption A is irreducibility (Matrix.IsIrreducible) of every such chain matrix. Assumption B is reachability of $L$ from every state; for a finite chain in which $L$ is absorbing, this is equivalent to absorption with probability one. $Q_R(i)$ is a real limsup of a bounded sequence, with the paper's sum over $t = 0, \dots, T$. $S_R(i)$ takes values in $[0, \infty]$. The paper requires $w_{ik} > 0$ on p. 17 and $w_{Lk} = 0$ in Problem 2. The formalization uses $w_{ik} > 0$ for $i \ne L$ in Problem 2, and keeps the two problems as separate implications. The adjoined state $-1$ is none : Option S, with the transition law that produces Derman's $p_{-1,i} = 1/(L+1)$, $p_{L,-1} = 1$ for every procedure. The published JewellMRP.InfiniteStep definitions of an ergodic matrix and of a stationary vector are reused.

The goal states optimality of the decoded procedure against every competitor in $C'$, for every optimal solution of the linear program, with existence of an optimal solution as a separate clause. A statement that only identifies feasible sets, or that only asserts that some optimal procedure exists, does not count as Theorem 2. Optimality over all history-dependent procedures is Theorem 1, a separate mission of this series.

Welcome contributions: the stationary-distribution facts for irreducible finite stochastic matrices (reusable across Markov chain work), a small linear-programming existence lemma (a linear function attains its minimum on a nonempty compact polytope), and the Lemma's transformation, which is self-contained.

Selected references

• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4):181–186, 1962. https://doi.org/10.1002/nav.3800090303
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$: gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$. The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from 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)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$. The vector $\beta$ is $S$-sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

$$(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$$

for all $|T|\le S$ and all coefficient vectors $c$; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$, $|T'|\le S'$.

Given a tuning parameter $\lambda_p>0$, the 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}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .$$

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$, $3S\le p$, $\beta$ $S$-sparse, and $\delta_{2S}+\theta_{S,2S}<1$. For every $a\ge0$, with $\lambda_p=\sqrt{2(1+a)\log p}$, with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

$$\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .$$

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$, display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

1. The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$, then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$.
2. The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$.
3. Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ($T_1$ the $S$ largest entries of $h$ off $T_0$) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$, and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$.
4. The deterministic core: with $\sigma=1$, on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$, every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$.
5. The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$, $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$.

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$, the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$. The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$-sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$. Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$-recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$, while its proof gives $\delta_{2S}$ in place of $\delta_S$.

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$, $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$; the goal is stated for general $\sigma>0$.

Committed conventions and corrections:

• Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$, but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$. Since $\delta_S\le\delta_{2S}$, the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$.
• Domain. $1\le S$ and $3S\le p$, because $\theta_{S,2S}$ is defined only for $S+2S\le p$. This forces $p\ge3$ and $\log p>0$.
• Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
• Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$.

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$, not on free parameters, and it is satisfiable (for instance by $X=I_p$, where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

• E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
• E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
• P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below $3/2$ unless P = NP. The natural question is therefore asymptotic: how small can the additive error $A(I) - OPT(I)$ be made, as a function of the optimum $OPT(I)$?

• 1974: D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey and R. L. Graham analysed First Fit and First Fit Decreasing, with asymptotic ratios $17/10$ and $11/9$ (SIAM J. Comput. 3(4)).
• 1981: W. Fernandez de la Vega and G. S. Lueker gave an asymptotic approximation scheme: for every $\varepsilon > 0$, $(1+\varepsilon)\,OPT(I) + 1$ bins in linear time (Combinatorica 1).
• 1982: N. Karmarkar and R. M. Karp replaced the multiplicative error by an additive one: $OPT(I) + O(\log^2 OPT(I))$ bins in polynomial time (Proc. 23rd FOCS). This mission formalizes that bound.
• 2017: R. Hoberg and T. Rothvoss improved the additive error to $O(\log OPT)$ (SODA 2017). Whether $OPT(I) + O(1)$ is achievable remains open.

Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.

Setting

An instance $I$ is a finite multiset of piece sizes in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, $SIZE(I)$ for the total size and $a(I)$ for the smallest size. A packing is a multiset of bins whose union is $I$ and in each of which the sizes sum to at most $1$; its cost is the number of bins, and $OPT(I)$ is the least cost.

A configuration is a nonempty multiset of sizes occurring in $I$ that fits in one bin. The fractional bin-packing problem is the linear program

$$(I)\qquad \min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x \ge 0,\quad Ax \ge b,$$

with one variable $x_j$ per configuration, where $A_{tj}$ counts the pieces of size $t$ in configuration $j$ and $b_t$ the pieces of size $t$ in $I$. Its value is $LIN(I)$. A basic feasible solution is an extreme point of the feasible region.

Geometric grouping with parameter $k$ sorts the pieces in non-increasing order and cuts them into consecutive groups $G_1, G_2, \dots, G_q$, each the shortest run of pieces of total size at least $k$. Within each group $G_i$ ($i \ge 2$) only as many of the largest pieces as $G_{i-1}$ has are kept; they are rounded up to the largest size in $G_i$, giving $G_i'$. The rounded pieces form $J$, and $G_1$ together with the unrounded leftovers $\Delta G_i$ form $J'$.

ALGORITHM 2 with a positive integer $k$ and a positive real $g$:

1. Eliminate all pieces of size $\le g$.
2. While $SIZE > 1 + \frac{1}{1-1/k}\ln\frac1g$: group the current instance into $J, J'$; pack $J'$ in at most $2k[2 + \ln\frac1g]$ bins; obtain a basic feasible solution $x$ of the LP of $J$ with cost at most $LIN(J)+1$; open $\lfloor x_j\rfloor$ bins of each configuration $j$, fill them with pieces, and delete the pieces so packed.
3. Pack the remaining pieces in at most $2 + \frac{2}{1-1/k}\ln\frac1g$ bins.
4. Reinsert the eliminated pieces, using a new bin only when necessary.

Its cost on $I$ is written $A(I)$.

Formalization targets

Goal: Theorem 4 with explicit constants

For every instance $I$ with $SIZE(I) \ge 2$, every packing that ALGORITHM 2 with $k=2$ and $g = 1/SIZE(I)$ can output is a packing of $I$ with

$$A(I) \le OPT(I) + \bigl(1 + \log_2 OPT(I)\bigr)\bigl(9 + 4\ln OPT(I)\bigr) + 2 + 4\ln OPT(I).$$

This is the paper's $A(I) \le OPT(I) + O(\log^2 OPT(I))$, with the constants that its proof yields.

The general bound for ALGORITHM 2

For integers $k \ge 2$, $0 < g \le \tfrac12$ and $SIZE(I) \ge 1$:

$$A(I) \le \max\Bigl\{(1+2g)\,OPT(I) + 1,\ OPT(I) + \Bigl[1 + \frac{\ln SIZE(I)}{\ln k}\Bigr]\Bigl[1 + 4k + 2k\ln\frac1g\Bigr] + 2 + \frac{2}{1-\frac1k}\ln\frac1g\Bigr\}.$$

Milestones

In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on $J'$, item 4 corrected); the per-iteration shrinking of $SIZE$; the bound on the number $t$ of iterations; the telescoping of $LIN$; the bin count after Step 3; the general bound.

Significance

The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme ($O(\log^2 OPT) = o(OPT)$). Varying $k$ and $g$ trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the $O(\log OPT)$ bound of Hoberg and Rothvoss.

The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.

Difficulty

Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most $m$ fractional variables, and after rounding down, the leftover pieces form an instance of size at most $m(J)$. With linear grouping that leftover is of order $1/\varepsilon^2$ and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance $J$ with $m(J) \le SIZE/k + O(\ln(1/g))$ distinct sizes while discarding only $O(k\ln(1/g))$ in $J'$. The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in $SIZE$, $LIN$ and $OPT$, with an additive loss per iteration; the harmonic-sum estimate behind $SIZE(J')$ and the telescoping of $LIN$ across iterations carry most of the weight.

Formalization scope

• Model. An instance is a Multiset ℝ with sizes in the open interval $(0,1)$; real sizes generalize the paper's rationals, and the interval is open because a group of size at least $k$ must contain more than $k$ pieces. Packings are Multiset (Multiset ℝ). $OPT$ and $LIN$ are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.
• Subroutine contract. The Fractional Bin-Packing procedure is modelled only by its stated output: any basic feasible solution of cost at most $LIN(J)+1$. The ellipsoid method of §6 is not modelled.
• Runs. ALGORITHM 2 is a relation Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.
• Explicit constants. $O(\log^2 OPT(I))$ in Theorem 4 is replaced by $(1+\log_2 OPT)(9 + 4\ln OPT) + 2 + 4\ln OPT$. The asymptotic threshold is made explicit as $SIZE(I) \ge 2$. $\ln$ is Real.log and $\log_2$ is Real.logb 2.
• Corrected statements. The last group of geometric grouping may fall short of $k$, which the paper ignores. For it, $\Delta G_q$ consists of the $\max(0, l_q - l_{q-1})$ smallest pieces. Theorem 2, item 4 is stated as $m(J) \le SIZE(J)/k + \ln(1/a(I)) + 1$; the printed version without $+1$ fails for $I = \{0.95, 0.95, 0.95, 0.9\}$, $k = 2$. Theorem 2 is stated for integers $k \ge 2$, which its proof needs. The iteration bound is stated for $t \ge 1$ and for the instance after Step 1.
• Out of scope. Running times, polynomiality, the function $T(m,n)$, the number of subroutine calls, §6, ALGORITHM 3 and Theorem 5.
• Ruling out trivial versions. "There exists a packing with at most $OPT(I) + \dots$ bins" is trivially true and is not the goal. The goal bounds every output of the algorithm, and the existence item shows that outputs exist.

Contributions welcome: milestone proofs; a harmonic-sum bound $\sum_{j=a}^{b} 1/j \le \ln\frac{b}{a-1}$; extreme-point facts for $\{x \ge 0 : Ax \ge b\}$ (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of $LIN$ and $OPT$ under the piecewise order.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), IEEE, pp. 312–320, 1982. https://doi.org/10.1109/SFCS.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1 + ε in linear time, Combinatorica 1(4), 349–355, 1981. https://doi.org/10.1007/BF02579456
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-case performance bounds for simple one-dimensional packing algorithms, SIAM J. Comput. 3(4), 299–325, 1974. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoss, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. 28th ACM-SIAM SODA, 2616–2625, 2017. https://doi.org/10.1137/1.9781611974782.172

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$–$1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$. The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$, and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$.

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$, or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

$$\sum_{A\in\mathbf L}q(A)=\min_{B\in b(\mathbf L)}\sum_{x\in B}w(x).$$

For a set $Z$, the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

$$Q_6=\{\{1,3,5\},\{1,4,6\},\{2,3,6\},\{2,4,5\}\},$$

the triangles of $K_4$ with its edges labelled $1,\dots,6$.

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$. With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$, $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$. In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$, and $y$ is initial if no $x$ has $x\to y$. MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$,

$$\mathbf L\ \text{is Mengerian}\iff \mathbf L\ \text{has no minor isomorphic to } Q_6 .$$

Milestones

In the order the proof uses them:

• (2.3) Every minor of a Mengerian clutter is Mengerian.
• Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
• (3.6)(i) Circuits of a binary clutter have at least two elements.
• (3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$.
• (4.3) In a critical MBC, $x\to y$ implies $y\not\to x$.
• (4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$, $z\to y$ for $z\in C-\{y\}$, and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$.
• (4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$, and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$.
• (4.6) A nontrivial critical MBC has a member consisting of initial elements.
• (5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$, together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$, $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$-free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$. Weights $w$ and packings $q$ are $\mathbb N$-valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$, which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$, dropping the $\{\emptyset\}$ exception, and reading "$Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$. The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$, (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

• P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105