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

Motivation

Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.

The potential carries a parameter $\rho > n$. The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give $O(\sqrt n\,t)$ iterations with $\rho = n + \Theta(\sqrt n)$. Practical codes, however, performed better with much larger $\rho$ (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With $\rho = n + \Theta(n^2)$ and the step chosen to minimise the potential inside the wide neighbourhood $\mathcal N_\infty^-(\beta)$, the method needs $O(nt)$ iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).

Timeline:

• 1990: Todd and Ye introduce the primal–dual potential function.
• 1989–1991: Kojima–Mizuno–Yoshise, Ye, Freund and others prove $O(\sqrt n\,t)$ bounds for $\rho = n + \Theta(\sqrt n)$.
• 1990–1991: Mizuno, Todd and Ye prove the $O(nt)$ bound for $\rho = n + \Theta(n^2)$ (Theorem 3 of the report formalized here).

Setting

Fix $m \ge 0$, $n \ge 1$, $A \in \mathbb R^{m\times n}$, $b \in \mathbb R^m$, $c \in \mathbb R^n$. The primal problem is $\min c^Tx$ subject to $Ax = b$, $x \ge 0$. The dual is $\max b^Ty$ subject to $A^Ty + s = c$, $s \ge 0$. The strictly feasible set $\mathcal F^0$ is the set of pairs $(x, s)$ with $x > 0$, $s > 0$, $Ax = b$ and $A^Ty + s = c$ for some $y$. The duality measure is $\mu = x^Ts/n$.

For $z \in \mathbb R^n$ put $(z^-)_j = \min\{z_j, 0\}$ and $\|z\|_\infty^- = \|z^-\|_\infty$. For $\beta \in (0,1)$, the wide neighbourhood is

$$\mathcal N_\infty^-(\beta) = \{(x,s) \in \mathcal F^0 : \|Xs - \mu e\|_\infty^- \le \beta\mu\},$$

i.e. $x_js_j \ge (1-\beta)\mu$ for all $j$, where $X = \mathrm{diag}(x)$ and $e$ is the all-ones vector.

The potential is

$$\psi(x,s) = \rho\log(x^Ts) - \sum_{j=1}^n \log(x_js_j), \qquad \rho > n,$$

with the natural logarithm. At $(x,s)$ and for $\gamma \in (0,1)$, a search direction $d = (d_x, d_y, d_s)$ solves

$$S d_x + X d_s = \gamma\mu e - Xs,\qquad A d_x = 0,\qquad A^Td_y + d_s = 0,$$

and the iterates move along $x(\theta) = x + \theta d_x$, $s(\theta) = s + \theta d_s$. The scaled vectors are $p_j = \sqrt{s_j/x_j}\,(d_x)_j$ and $q_j = \sqrt{x_j/s_j}\,(d_s)_j$, $Pq = (p_jq_j)_j$, and $\theta_2^- = \min\{1, \beta\gamma\mu/\|Pq\|_\infty^-\}$.

Algorithm 3. Start from $(x^0,s^0) \in \mathcal N_\infty^-(\beta)$ with $(x^0)^Ts^0 \le 2^t$ and $\psi(x^0,s^0) \le (\rho-n)t + n\log n$. While $(x^k)^Ts^k > 2^{-t}$, compute $d$ at $(x^k, s^k)$, choose $\bar\theta$ with $(x(\bar\theta), s(\bar\theta)) \in \mathcal N_\infty^-(\beta)$ and $\psi(x(\bar\theta), s(\bar\theta)) \le \psi(x(\theta), s(\theta))$ for every $\theta$ with $(x(\theta), s(\theta)) \in \mathcal N_\infty^-(\beta)$, and move to $(x(\bar\theta), s(\bar\theta))$.

Formalization targets

Goal: Theorem 3 (p. 11)

Let $\beta,\gamma \in (0,1)$ with $\gamma \le 2(1-\beta)$ and

$$\rho = n + \Bigl(\frac{3}{\beta\gamma(1-\gamma)}\log\frac{1}{1-\beta}\Bigr)n^2.$$

For every $t > 0$ and every run of Algorithm 3,

$$\exists\, k \le \Bigl\lceil \frac{6nt}{11\beta\gamma(1-\gamma)} \Bigr\rceil:\quad (x^k)^Ts^k \le 2^{-t}.$$

The paper states "$O(nt)$ iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.

Milestones

1. §5, p. 11. $\psi(x,s) = (\rho-n)\log(x^Ts) - \sum_j\log\frac{x_js_j}{x^Ts/n} + n\log n \ge (\rho-n)\log(x^Ts) + n\log n$. Hence reducing $\psi$ to $-(\rho-n)t + n\log n$ gives $x^Ts \le 2^{-t}$.
2. (16), p. 12. One step of Algorithm 3 satisfies $\psi(x(\bar\theta),s(\bar\theta)) - \psi(x,s) \le -\bigl(\frac{3n^2\theta_2^-}{\beta\gamma} - n\bigr)\log\frac{1}{1-\beta}$.
3. Proof of Theorem 3, p. 12. For $n \ge 1$, every step decreases $\psi$ by at least $11n\log\frac{1}{1-\beta}$.

Significance

The result shows that a potential-reduction method with $\rho - n$ of order $n^2$ keeps a polynomial worst-case bound. The earlier analyses cited by the report used $\rho - n$ of order $\sqrt n$. It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term $Pq$ decrease the potential far more.

The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step $\theta_2^-$ in $\mathcal N_\infty^-(\beta)$, the potential decrease (16), and the complexity bound.

Difficulty

The step $\bar\theta$ is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term $Pq$ of the Newton direction in the one-sided norm $\|\cdot\|_\infty^-$, together with the centrality of the current iterate. A fixed decrease of order $n$ arises only because $\rho - n$ is of order $n^2$. Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.

A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real $\theta$ whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.

Formalization scope

Vectors are Fin n → ℝ, with index $j = 1,\dots,n$ mapped to Fin n; $\|\cdot\|_\infty$ is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. $\psi$ is the published definition LinearOptimization.interiorPointPotential with $q := \rho$. It equals (1) at every strictly positive pair, and it is evaluated only at points of $\mathcal N_\infty^-(\beta)$. All logarithms are natural, and $2^{\pm t}$ are real powers with real $t > 0$. A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds $2^{-t}$, the step relation of Algorithm 3. Iterates after termination are unconstrained.

Conventions and repairs:

• $\theta_2^- := 1$ when $\|Pq\|_\infty^- = 0$, reading $\beta\gamma\mu/0$ as $+\infty$.
• The per-iteration milestone keeps the page's $n \ge 1$. The paper's step $\theta_2^- \ge 4\beta\gamma/n$ needs $4\beta\gamma \le n$, which can fail for $n = 1$; but for $n = 1$ the potential is unbounded below along the line inside the neighbourhood, so no step exists and the statement holds vacuously there. The goal keeps $n \ge 1$ as well.
• The minimisation in Algorithm 3 ranges over all real $\theta$, as printed. It does not range over a segment, and the step is not the largest admissible step of Algorithm 2.
• Both start conditions are kept: $(x^0)^Ts^0 \le 2^t$ from Algorithm 2 and the potential bound of §5.

A formalization in which no run can exist for any instance, or in which $\rho$ or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for $n \ge 2$ whenever the potential attains its minimum along the line, and the count is the explicit expression above.

Needed infrastructure: the algebra of system (2), namely $d_x^Td_s = 0$, the identity $\mu(\theta) = (1-(1-\gamma)\theta)\mu$, and $X(\theta)s(\theta) - \mu(\theta)e = (1-\theta)(Xs - \mu e) + \theta^2 Pq$. Also needed are the bounds $\|Pq\|_\infty \le \|r\|^2/4$ and $\|r\|^2 \le n\mu$ on $\mathcal N_\infty^-(\beta)$ when $\gamma \le 2(1-\beta)$, and the arithmetic–geometric mean inequality for $\psi$. These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.

Selected references

• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944, 1990, rev. 1991; Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• M. J. Todd, Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15(3):508–529, 1990. https://doi.org/10.1287/moor.15.3.508

Motivation

Many combinatorial optimization problems ask for the largest value of a linear objective over discrete feasible solutions. A linear program over the convex hull of those solutions has the same optimum, so one approach is to describe that hull by inequalities. For matching, for example, inequalities support efficient optimization; for other problems, the full family can be very large. A generator of violated inequalities offers a different interface: given a proposed point, it either certifies hull membership or produces one valid inequality that the point violates. Karp and Papadimitriou asked what the existence of an efficient generator implies for the underlying decision problem. Their answer is Theorem 2 of the technical report.

The report appeared as MIT/LCS/TM-154 in 1980 and later in SIAM Journal on Computing in 1982. Its first theorem addresses a small facial description whose inequality family belongs to NP. This mission concerns its second theorem, where the inequalities may be generated on demand in polynomial time. The conclusion is stronger: the decision language itself belongs to P. The report derives an NP-complete consequence as Corollary 2, conditional on the unresolved equality P = NP. The published article gives the later bibliographic record; all numbering here follows the technical report.

Setting

A combinatorial optimization problem $C=(L,n,S)$ consists of a binary input language $L$, a nonnegative integer dimension $n(z)$, and a set $S(z)\subseteq\mathbb Z_+^{n(z)}$ of feasible vectors for each $z\in L$. The report requires polynomial-time recognition of $L$, of correctly sized pairs $\langle z,y\rangle$, and of feasible pairs $\langle z,x\rangle$. An instance adds an integer objective $c\in\mathbb Z^{n(z)}$. Its threshold decision language is

$$D(C)=\{\langle z,c,k\rangle:z\in L,\ k\in\mathbb Z,\ \exists x\in S(z),\ c\cdot x\ge k\}.$$

Write $\mathrm{CH}(S(z))$ for the convex hull of the feasible vectors. A generator $G(C)$ receives $z\in L$ and a rational vector $p\in\mathbb Q^{n(z)}$. It returns “O.K.” exactly when $p$ belongs to the hull. Otherwise it returns an integer vector $f$ and integer $g$ for which $f\cdot p>g$ while $f\cdot x\le g$ for every $x\in S(z)$. The family $F_G(C)$ contains every triple $\langle z,f,g\rangle$ that occurs as some output. It is a facial description because its inequalities describe the hull exactly. The generator is small if one polynomial $p_0$ bounds every coefficient in every output by $2^{p_0(|z|+n(z))}$ in absolute value. Its running time is measured on the full encoded query, including every rational coordinate. These definitions are from §§2 and 4 of the report.

Formalization targets

Theorem 2

The goal is the report's stated implication:

$$G(C)\text{ is a small polynomial-time generator}\quad\Longrightarrow\quad D(C)\in\mathrm P.$$

It allows any c.o.p. satisfying Definition 1, including an empty feasible set or dimension zero. It does not assert P = NP; that consequence needs the additional hypothesis that $D(C)$ is NP-complete. The goal is supported by five source claims: the output family is facial; feasibility of system (4) is equivalent to membership in $D(C)$; Lemma 4 bounds the distance from a rational point to a small hyperplane; its Corollary extends the bound to a real point on a flat; and Lemma 5 controls distance to a flat after one more hyperplane is added. The system (4) target is

$$\exists x\in\mathbb Q^{n(z)}:\quad c\cdot x\ge k,\quad f\cdot x\le g\quad(\langle z,f,g\rangle\in F_G(C))\quad\Longleftrightarrow\quad\langle z,c,k\rangle\in D(C).$$

The distance targets use the report's parameter $t$ and the bounds $2^{-(n(z)+1)t}$ and $(2^t-1)\delta$, exactly as printed on pp. 12–13.

Significance

Theorem 2 turns an efficient separation interface into an efficient test for the threshold language. Consequently, if a c.o.p.'s decision language is NP-complete, a small polynomial-time generator would imply P = NP, as the report's Corollary 2 says. This gives a complexity barrier to a whole class of proposed cutting-plane interfaces, independently of how many inequalities the complete description contains. The result concerns the worst-case running time and output coefficient size; it does not rule out useful generators without those guarantees. Karp and Papadimitriou also point out positive applications to problems already known to be in P.

The mathematical theorem was proved in the report. The mission asks for a machine-checked version of that known result, with explicit interfaces for the generator, coefficient bounds, and the underlying complexity class. The local platform catalog already contains Cook's Turing-machine definitions and a reusable binary-integer encoding; it also contains point-to-hyperplane distance results and a Gram-determinant distance result in other settings. Theorem 2 and these particular source claims are new formalization targets here. The distance and encoding interfaces can serve later missions about separation oracles and bit complexity.

Difficulty

Calling the generator once does not by itself decide whether the objective threshold is attainable: the point supplied to it may be outside the hull, and a single returned inequality says only that this point is excluded. Repeatedly asking at an unchanged point may return the same inequality. The report must also control very small separations, coefficient sizes, and finite precision when an iterative linear-feasibility procedure uses the oracle. Lemmas 4 and 5 quantify the geometric gaps and movement that such a procedure needs. Its Lemmas 2, 3, and 6 address the surrounding perturbation, volume, and iteration arguments; Lemma 6 explicitly relies on another analysis for the finite-precision bound. These are substantive proof obligations even though their statements are not all separate milestones in this proposal. See §4 of the report.

Formalization scope

The report's footnote uses $R$ for the rationals. Thus $p$, the hull, and system (4) live in $\mathbb Q^{n(z)}$. Euclidean distances are evaluated after casting coordinates into $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\ n)$; a hyperplane distance is the quotient $|f\cdot r-g|/\|f\|_2$, and distance to a flat uses Euclidean infimum distance. The report does not define “affinely independent hyperplanes”; this mission reads it as linear independence of their normals, which ensures a common flat. Small hyperplanes have nonzero normals, avoiding a zero denominator.

The alphabet is $\{0,1,-,\#\}$. Binary tuple codes contain $z$, an explicit vector dimension, and every integer; a rational coordinate contains its reduced numerator and denominator. The generator's string function must match the mathematical oracle on every valid query and be polynomial time in the complete code length. A malformed string is outside $D(C)$. The source's arbitrary polynomial bound is written $m^a+a$ for one exponent $a$ fixed before all instances. For the bit-length parameter $t$, the printed logarithms of possibly nonpositive $c_i$ and $k$ are read as ceiling logarithms of absolute values, with $\operatorname{clog}_2(0)=0$ and the printed $+1$ terms retained. The source's formula $\varepsilon=2^{-(2n(z)+2)t}$ remains relevant to the eventual proof of Theorem 2, although no $\varepsilon$ system is a separate draft item here.

Every oracle answer must separate the queried point and remain valid on all of $S(z)$; these obligations prevent an arbitrary function from satisfying the goal. The c.o.p. structure retains all three polynomial-recognition conditions of Definition 1. The paper's displayed “min” in (3) is inconsistent with its threshold language and surrounding maximization formulas; $D(C)$ uses the printed $c\cdot x\ge k$. The typed source's “$x\notin H$” in Lemma 4 is read as the already named point $r\notin H$.

Contributions can develop the rational-hull equivalence, the two quantitative hyperplane lemmas, the finite-precision ellipsoid procedure underlying Lemma 6, or the perturbation and volume claims. The complexity substrate is Cook's one-tape model of P and NP, and the binary integer codec is the published ProjSchedTW_Complexity_Encoding definition. The geometry lemmas are phrased so that existing Mathlib Euclidean-space results can be reused without changing the source's rational optimization domain.

Selected references

• Richard M. Karp and Christos H. Papadimitriou, On Linear Characterizations of Combinatorial Optimization Problems, MIT/LCS/TM-154, Massachusetts Institute of Technology, 1980. Technical report.
• Richard M. Karp and Christos H. Papadimitriou, “On Linear Characterizations of Combinatorial Optimization Problems,” SIAM Journal on Computing 11 (1982), 620–632. DOI.
• Stephen A. Cook, “The Complexity of Theorem-Proving Procedures,” Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971. DOI.

Motivation

Polyhedral combinatorics attacks a combinatorial optimization problem by replacing its finite set of feasible solutions with the convex hull of that set and describing the hull by linear inequalities. Once such a description is known, the problem becomes a linear program, and linear programming duality supplies optimality certificates. For matchings, matroids and network flows this programme succeeded completely (Edmonds' matching polytope is the classical example). For the traveling salesman problem, set covering and integer programming, decades of work produced large families of valid and facet-defining inequalities but never a complete list.

R. M. Karp and C. H. Papadimitriou asked whether the failure is accidental. Their answer, in the MIT technical report On linear characterizations of combinatorial optimization problems (MIT/LCS/TM-154, February 1980; journal version SIAM J. Comput. 11 (1982) 620–632), is that for NP-complete problems a usable complete description cannot exist unless NP = co-NP. This mission formalizes the first of their two complexity results, Theorem 1, together with the steps of its proof and its Corollary 1.

Setting

A combinatorial optimization problem (c.o.p.) $C$ consists of a set $L\subseteq\{0,1\}^*$ of inputs, a function $n$ assigning to each input $z\in L$ a number of variables $n(z)\ge 0$, and for each $z\in L$ a set $S(z)\subseteq(\mathbb Z^+)^{n(z)}$ of nonnegative integer vectors, the feasible solutions. The three languages $L$, $\{\langle z,y\rangle : |y|=n(z)\}$ and $\{\langle z,x\rangle : x\in S(z)\}$ must be recognizable in polynomial time. An instance is a pair $\langle z,c\rangle$ with $z\in L$ and $c\in\mathbb Z^{n(z)}$, and the decision problem of $C$ is

$$D(C)=\{\langle z,c,k\rangle : z\in L,\ c\in\mathbb Z^{n(z)},\ k\in\mathbb Z,\ \exists x\in S(z)\ \ c\cdot x\ge k\}.$$

Write $\mathrm{CH}(S(z))\subseteq\mathbb Q^{n(z)}$ for the convex hull of $S(z)$ over the rationals. A facial description of $C$ is a set $F(C)$ of triples $\langle z,f,g\rangle$, with $z\in L$, $f\in\mathbb Z^{n(z)}$ and $g\in\mathbb Z$, such that for every $z\in L$ and every $x\in\mathbb Q^{n(z)}$

$$x\in\mathrm{CH}(S(z))\iff f\cdot x\le g\ \text{ for all }\langle z,f,g\rangle\in F(C).$$

It is small if for some polynomial $p$ every component of every triple $\langle z,f,g\rangle\in F(C)$ has absolute value at most $2^{p(|z|+n(z))}$, so that each coefficient has polynomially many bits. The statement $F(C)\in\mathrm{NP}$ means that the language of the triples of $F(C)$ is in NP: membership of a listed inequality has short, checkable proofs.

Formalization targets

Goal: Theorem 1 (p. 7)

$$F(C)\ \text{a small facial description of }C,\quad F(C)\in\mathrm{NP}\ \Longrightarrow\ D(C)\in\text{co-NP}.$$

Milestones, in the order the proof uses them

1. (p. 5) For a small facial description and every $z\in L$, only finitely many triples have first entry $z$, and $\mathrm{CH}(S(z))$ is the intersection of finitely many half-spaces.
2. (pp. 7–8, (i)⇔(ii)) $\langle z,c,k\rangle\notin D(C)$ iff $c\cdot x<k$ for every $x\in\mathrm{CH}(S(z))$.
3. (p. 8, (ii)⇔(iii)) For a facial description, the same holds with $\mathrm{CH}(S(z))$ replaced by the system $f\cdot x\le g$, $\langle z,f,g\rangle\in F(C)$.
4. (p. 8, (iii)⇔(vi)) For a small facial description and $S(z)\neq\emptyset$: $c\cdot x<k$ on that system iff there are $n(z)$ triples $\langle z,f_i,g_i\rangle\in F(C)$ whose matrix $\mathbf F$ is nonsingular and the solution $y$ of $y^T\mathbf F=c$ satisfies $y\ge 0$ and $y^Tg<k$.

After the goal: Corollary 1 (p. 8)

$$D(C)\ \text{NP-complete},\ F(C)\ \text{small facial},\ F(C)\in\mathrm{NP}\ \Longrightarrow\ \mathrm{NP}=\text{co-NP}.$$

Significance

Theorem 1 converts a question of polyhedral combinatorics into one of complexity theory. Corollary 1 then says that for the traveling salesman problem, Hamiltonian circuit, set covering, integer programming and every other c.o.p. with an NP-complete decision problem, no complete linear description of the hulls has both polynomially sized coefficients and polynomially verifiable membership, unless NP = co-NP. This explains why the search for complete descriptions of such polytopes has not succeeded and why research on them turned to partial descriptions and separation. The companion result of the same paper (Theorem 2, the subject of the second mission in this series) treats separation routines and P instead of facial descriptions and co-NP.

The result itself is proved, by a short argument in the paper. To our knowledge it has no machine-checked proof. Formalizing it requires connecting three things that the platform holds only separately: Cook's Turing-machine classes P, NP and co-NP (published as CookPvsNP_defs), linear programming duality over the rationals (Farkas' lemma is published, e.g. LinearOptimization.farkas_inequality_form_fintype, for real matrices), and polynomial-time arithmetic on binary-encoded rational data, such as solving a nonsingular integer linear system. The last ingredient, a polynomial-time verifier built from a polynomial-time recognizer, is reusable for every co-NP or NP membership proof on the platform.

Difficulty

The mathematical content of Theorem 1 is the duality chain (i)⇔(vi): the "no" answer is certified by $n(z)$ inequalities of $F(C)$ and a basic dual solution. Two points make the formal proof harder than the paper's page suggests.

First, the duality chain needs care at its edges. When $S(z)$ is empty the chain (iii)⇔(vi) can fail, so the verifier must also accept a different certificate (an infeasibility certificate from at most $n(z)+1$ triples), while milestone 4 carries the hypothesis $S(z)\neq\emptyset$. Pointedness of the hull, which follows from $S(z)\subseteq(\mathbb Z^+)^{n(z)}$, is what guarantees $n(z)$ linearly independent rows.

Second, "Algorithm B clearly runs in polynomial time" hides a complete complexity argument on Cook's one-tape machines: parsing the input, testing $z\in L$ and $|c|=n(z)$ with the recognizers of Definition 1, guessing the matrix within the size bound given by smallness, invoking the NP verifier of $F(C)$ $n(z)$ times, and solving $y^T\mathbf F=c$ exactly over $\mathbb Q$ with polynomially bounded bit sizes (Cramer's rule bounds the numerators and denominators of $y$). The certificate must be of length polynomial in the input, which uses the uniform polynomial in the definition of "small". The naive certificate, a single optimal vertex of the hull, does not work: it proves a "yes" answer, not a "no".

Formalization scope

All definitions live in the namespace KarpPapadimitriou.Facial. Strings are List Bool; $S(z)$ is a set of Fin (n z) → ℤ with nonnegative entries; $\mathrm{CH}(S(z))$ is convexHull ℚ of its image in Fin (n z) → ℚ, because the paper's "R" denotes the rationals (footnote, p. 3). Tuples are coded over the four-letter alphabet $\{0,1,-,\#\}$ of the published ProjSchedTW_Complexity_Encoding, integers in binary, vectors prefixed by their length so that codes are uniquely decodable. P, NP, co-NP and NP-completeness are the published CookPvsNP_defs; $D(C)$ and the triple language of $F(C)$ are sets of codes, so strings encoding no triple lie in the complement of $D(C)$, as in Algorithm B's step (i). The three polynomial-time conditions of Definition 1 are fields of the structure COP.

Explicit readings of the paper's loose phrases:

• "polynomial $p$" in "small" is $m\mapsto m^k+k$ with one $k$ for all triples;
• "has optimal value $<k$" for (ii) and (iii) is "every feasible point has value $<k$", meaningful for infeasible and unbounded programs;
• "the system $y^T\mathbf F=c$ has a unique nonnegative solution $y$ with $y^Tg<k$" is "$\det\mathbf F\neq0$ and the solution satisfies $y\ge 0$, $y^Tg<k$";
• (iii)⇔(vi) carries the hypothesis $S(z)\neq\emptyset$, tacit in the paper; Theorem 1 does not;
• "NP = co-NP" in Corollary 1 holds for every finite nonempty alphabet, since Cook's classes are indexed by the alphabet.

Printed slips: display (3) reads "min" while $D(C)$ and the proof maximize; Algorithm B's step (v) reads "$y^Tb>k$" for $y^Tg<k$. Both are formalized in the corrected sense.

A trivializing formalization is ruled out: the goal quantifies over every c.o.p. and every small facial description, with complements taken over all strings, and no hypothesis restricts $S(z)$ or $F(C)$ beyond Definition 1 and the definitions of p. 4–5. Claim 1 (p. 9), announced without proof, is not part of the mission.

Contributions welcome: proofs of the four milestones (milestone 4 is an exercise in rational LP duality on finite systems), a reusable library of polynomial-time integer and rational arithmetic on Cook's machines, and the closure of NP under polynomial-time reductions across alphabets that Corollary 1 needs.

Selected references

• R. M. Karp and C. H. Papadimitriou, On linear characterizations of combinatorial optimization problems, MIT/LCS/TM-154, February 1980. https://dspace.mit.edu/server/api/core/bitstreams/eb122126-c312-4445-a8d2-153e3e7d285f/content ; journal version SIAM J. Comput. 11 (1982) 620–632, https://doi.org/10.1137/0211053
• S. A. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (LP duality, basic solutions, sizes of solutions of linear systems). ISBN 978-0-471-98232-6
• M. Grötschel and M. W. Padberg, On the symmetric travelling salesman problem I: Inequalities, Math. Programming 16 (1979) 265–280. https://doi.org/10.1007/BF01582116

Motivation

The Hirsch conjecture, stated by Warren M. Hirsch in a 1957 letter to George Dantzig, asserts that the combinatorial diameter of a $d$-dimensional polytope with $n$ facets is at most $n-d$. The diameter is the largest number of edge steps needed to walk between two vertices of the polytope. The question matters to linear optimization: every edge-following pivot rule of the simplex method, starting at a vertex of the feasible region, needs at least as many pivots as the graph distance to an optimal vertex. A polynomial bound on polytope diameters is a necessary condition for a strongly polynomial simplex method, which is still unknown.

Timeline of the conjecture before the counterexample:

• 1967, Klee and Walkup: the conjecture fails for unbounded polyhedra, and for bounded polytopes it is equivalent to the $d$-step conjecture (the case $n=2d$). They also proved it for $n-d\le 5$.
• 1992, Kalai and Kleitman: a quasi-polynomial upper bound $n^{\log_2 d+2}$ on the diameter.
• 2010, Santos: a counterexample in dimension 43 with 86 facets (arXiv:1006.2814, published in Ann. of Math. 176 (2012) 383–412). It is the subject of this mission.
• 2012, Matschke, Santos and Weibel: smaller 5-dimensional spindles, giving counterexamples in dimension 20 (arXiv:1202.4701).

The polynomial Hirsch conjecture, which asks only for a bound polynomial in $n$ and $d$, remains open.

Setting

A polytope in $\mathbb R^d$ is written as $\mathrm{Hpoly}(a,b)=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$. A facet presentation is one in which $\mathrm{Hpoly}(a,b)$ has nonempty interior and no inequality is redundant. For a bounded polytope it then has dimension $d$, and its $n$ inequalities correspond one to one to its facets. A step between two vertices crosses an edge (a one-dimensional face). The polytope is non-Hirsch when its diameter exceeds $n-d$.

A spindle (Santos, Definition 1.4) is a polytope with two distinguished vertices $u,v$ such that every facet contains exactly one of them. Its length is the graph distance from $u$ to $v$. The polar objects are prismatoids: polytopes with two parallel facets $Q^+,Q^-$ containing all vertices, whose width is the dual-graph distance between $Q^+$ and $Q^-$.

Santos's explicit object is the 5-prismatoid $Q$ whose vertices are the 48 rows of Table 1 of the paper: $1^+,\dots,24^+$ with $x_5=1$ and $1^-,\dots,24^-$ with $x_5=-1$. Its polar $Q^\Delta=\{x\in\mathbb R^5:\langle r,x\rangle\le1\ \text{for each row } r\}$ is a spindle with apices $e_5$ and $-e_5$. Table 2 of the paper lists the 322 facets of $Q$, which are the 322 vertices of $Q^\Delta$: $\pm e_5$ and the points $\frac1{c_0}(\pm c_1,\pm c_2,\pm c_3,\pm c_4,c_5)$ of twenty types $B,B',\dots,K,K'$ with sixteen sign patterns each. The symmetry group $\Sigma$ of $Q$ has order 64; its index-two subgroup $\Sigma^+$ preserves $Q^+$ and $Q^-$.

Formalization targets

Goal: Corollary 1.7

$$\exists\, a:\mathrm{Fin}\,86\to\mathbb R^{43},\ b\in\mathbb R^{86}:\quad \mathrm{Hpoly}(a,b)\ \text{nonempty, bounded, a facet presentation, and}\ \operatorname{diam}\mathrm{Hpoly}(a,b)>43.$$

The goal fixes the dimension (43) and the number of facets (86), as the paper does. It does not assert the exact diameter (44, remarked on p. 24).

Milestones

1. §3, first bullet (polar form): $Q^\Delta$ is a bounded 48-facet spindle with apices $\pm e_5$, the rows tight at $e_5$ being $1^+,\dots,24^+$.
2. Theorem 4.1(1) (polar form): the 322 points of Table 2 are distinct vertices of $Q^\Delta$; the letter classes are $\Sigma^+$-orbits and the six $\Sigma$-orbits are A ∪ L, B ∪ K, C ∪ J, D ∪ I, E ∪ H, F ∪ G.
3. Theorem 4.1(2) (polar form): $Q^\Delta$ has no other vertices.
4. Theorem 3.1 (polar form): the distance from $e_5$ to $-e_5$ in the graph of $Q^\Delta$ is exactly 6.
5. Theorem 1.6: a 5-spindle with 48 facets, 322 vertices and length exactly six exists.
6. Inductive step of Theorem 2.6 (polar form): a $d$-spindle with $n>2d$ facets and length at least $l$ yields a $(d+1)$-spindle with $n+1$ facets and length at least $l+1$.
7. Theorem 1.5 (strong $d$-step theorem): a $d$-spindle with $n$ facets and length at least $l$ yields an $(n-d)$-spindle with $2n-2d$ facets and length at least $l+n-2d$, non-Hirsch when $l>d$.

Significance

Corollary 1.7 settles the Hirsch conjecture in the negative. Theorem 1.5 is the reusable part: it turns any spindle whose length exceeds its dimension into a counterexample. That made the later search for small spindles (Matschke–Santos–Weibel) a finite, low-dimensional problem. Theorem 1.6 is the concrete certificate. Its claims about Tables 1 and 2 are finite statements about explicit rational data.

The result is proved, and several pieces are already formalized on Prove2Me. Hirsch.santos_counterexample (Proved) states that some polytope violates the bound $n-d$, with no dimension or facet count. Hirsch.strong_dstep_spindle (Proved) is the "in particular" clause of Theorem 1.5, counting inequalities rather than facets. Lemmas 2.2 and 2.4 of the paper are Proved in polar form (Hirsch.spindle_inward_row_push_graph, Hirsch.spindle_wedge_vertex_graph_projection), as is the bound $n\ge2d$ for spindles (Hirsch.spindle_n_ge_two_d). This mission adds the dimension-43, 86-facet statement with facets counted exactly, the general length bound $l+n-2d$ with the spindle structure preserved, and a machine-checkable account of Santos's specific spindle.

Difficulty

The obvious first idea for the 5-dimensional milestones is brute computation. This is feasible in principle but heavy in Lean. Showing that 322 given points are extreme requires exhibiting, for each, five linearly independent tight rows among 48. Showing that no other vertex exists requires a complete enumeration argument rather than a membership check. Exact distance 6 requires the full adjacency structure between the 322 vertices, not only a path.

For the general theorems, the difficulty is that the construction is a one-point suspension followed by a perturbation. Edges and facets of the new polytope must be controlled, with the face lattice changing only in a prescribed way. Diameter is not monotone under arbitrary perturbations, and in particular a walk can become shorter. Keeping the facet count exact (not merely the inequality count) adds an irredundancy argument at each step.

Formalization scope

Polytopes are H-presentations Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d), from the platform definition Hirsch_model. "A $d$-polytope with $n$ facets" is boundedness plus IsFacetPresentation: nonempty interior and every row irredundant. Without this predicate, padding with redundant rows would change the bound $n-d$, and the statement would collapse to the platform's dimension-free Hirsch.santos_counterexample. Diameter and length use the platform's padded walks (Hirsch.DiamLE, Hirsch.Reach). "Length at least $L$" means no walk of fewer than $L$ steps, and "length exactly $L$" adds a walk of $L$ steps. The junk-valued Hirsch.gdist is never used.

All prismatoid statements of the paper (§3, Theorems 2.6, 3.1, 4.1) are stated for the polar spindle, which the paper licenses (pp. 6, 8, 9). Vertices of $Q$ become rows, facets of $Q$ become vertices, the width becomes the apex distance, and $Q^\pm$ become $\pm e_5$. Natural-number expressions $n-d$, $2n-2d$, $l+(n-2d)$ are faithful because spindles have $n\ge2d$. Theorem 1.5's "length $l$" is read as "length at least $l$", which is equivalent by monotonicity. Tables 1 and 2 are written entry by entry in Lean in the page's order.

Useful contributions include proofs of the finite Table 1/Table 2 facts by certified computation, reusable lemmas on one-point suspensions and on facet presentations under perturbation, and a proof of Corollary 1.7 from milestones 5 and 7.

Selected references

• F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012) 383–412; cited version arXiv:1006.2814v3. https://arxiv.org/abs/1006.2814 , https://doi.org/10.4007/annals.2012.176.1.7
• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967) 53–78. https://doi.org/10.1007/BF02395040
• G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://arxiv.org/abs/math/9204233
• B. Matschke, F. Santos and C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015) 647–672. https://arxiv.org/abs/1202.4701

Motivation

Chapter 6 built lift-and-project (L&P) cuts from a cut-generating LP, and Chapter 7 surveyed alternative nonlinear constructions reaching the same integer hull. This chapter asks a sharper question: how do L&P cuts relate, coefficient for coefficient, to older, more classical cutting planes — simple disjunctive cuts and mixed integer Gomory cuts, derived directly from a simplex tableau rather than from an auxiliary LP? The answer is an exact correspondence: every L&P cut from a basic solution of the cut-generating LP is equivalent to a specific simple disjunctive cut from a specific tableau basis, and conversely. This correspondence is not merely of theoretical interest — it converts a question about an infinite family of cuts into a finite, countable one (bases of a linear system), and it is what lets the chapter's capstone result, Theorem 8.7, establish a uniform rank bound of $p$ (the number of 0-1 variables) across four cut families at once, by proving it for one and transporting the proof to the other three.

Setting

$(CGLP)_k$ (eq. (8.1)) is the cut-generating LP for the disjunction $-x_k \ge 0 \lor x_k \ge 1$, with an added normalization constraint $ue+u_0+ve+v_0=1$ that makes its feasible polytope bounded — so a "basic solution" can be identified with an extreme point of that polytope. Given a basic solution with $u_0,v_0>0$ and basic $u/v$-components indexed by $M_1,M_2$ (Lemma 8.1-8.2), the $n\times n$ submatrix $\hat A$ of $\tilde A$ indexed by $J:=M_1\cup M_2$ is nonsingular, giving a simplex tableau in which $x_k$ is expressed as $x_k = \bar a_{k0} - \sum_{j\in J}\bar a_{kj}x_j$ (eq. (8.5)). The simple disjunctive cut from $x_k\le 0 \lor x_k\ge 1$ applied to this row has coefficients $\pi_j := \max\{\pi^1_j,\pi^2_j\}$, $\pi_0 := \bar a_{k0}(1-\bar a_{k0})$ (eq. (8.7)-(8.8)).

Formalization targets

Theorem 8.7 (goal) — a uniform rank bound across four cut families

The rank of the LP relaxation $P$ with respect to (a) unstrengthened L&P cuts, (b) simple disjunctive cuts, (c) strengthened L&P cuts, (d) mixed integer Gomory cuts (equivalently, strengthened simple disjunctive cuts) is at most $p$, the number of 0-1 variables.

The chain of results building toward it

Lemma 8.1 (basicness forces $u_0,v_0>0$), Lemma 8.2 (a basic solution's index sets give a nonsingular submatrix), Lemma 8.3 ($0<\bar a_{k0}<1$), Theorem 8.4A (a basic L&P cut equals a simple disjunctive cut), Theorem 8.4B (the converse: every simple disjunctive cut from a valid basis equals some basic L&P cut), and Theorem 8.5 (the same correspondence, strengthened).

Significance

The results themselves. Theorems 8.4A/8.4B are, in the book's own words, an "exact correspondence between lift-and-project cuts for a mixed 0-1 program and earlier cuts from the literature" — placing L&P cuts, simple disjunctive cuts, and (via Theorem 8.5) mixed integer Gomory cuts on the same logical footing, all generated by choosing a basis of one underlying linear system. Theorem 8.7 is the payoff: a single uniform bound covering four cut families that the literature had previously bounded (if at all) by separate arguments, and by contrast to the unbounded rank of pure-integer fractional Gomory cuts, exhibiting a case where the mixed 0-1 structure yields much stronger guarantees.

Formalizing it. No object in this mission exists on the platform prior to it or in Mathlib. This mission restates 06-lift-project-cuts's $(CGLP)$ apparatus and Theorem 6.4's strengthened cut formula locally, per the series convention that a draft mission cannot import another draft mission's definitions, adapted throughout to this chapter's normalized $(CGLP)_k$ and its disjunction on a single fixed coordinate $k$.

Difficulty

Formalizing "basic solution" required a genuine choice: unlike Chapter 6, $(CGLP)_k$'s normalization constraint makes its feasible set a bounded polytope, so this mission identifies "basic solution" with an extreme point of that polytope (Set.extremePoints) for Lemma 8.1 (whose own statement has no reference to specific index sets), while Lemmas 8.2 onward take the basic index sets $M_1,M_2$ directly as hypothesis data, matching how those theorems are themselves phrased ("let the basic components... be indexed by $M_1$ and $M_2$"). Theorem 8.7's rank bound required designing one generic HasRankAtMost predicate, parametrized by an abstract cut-closure operator, applicable uniformly to all four families — mirroring the book's own proof structure, which establishes the bound for one family and transports it to the other three via Theorems 8.4A/8.4B and 8.5, rather than arguing each part from scratch.

Formalization scope

The row/variable identification gap (see MODERATION_NOTES.md). The book's own eq. (8.4)- (8.5) identifies certain rows of the augmented, $m+p+n$-row matrix $\tilde A$ (those that are bound constraints $x_j\ge 0$) with the variables they bound, so that a chosen nonbasic row set $J$ doubles as a set of "nonbasic variables." This mission's abstract row type does not track that identification (matching the abstraction already used throughout 06-lift-project-cuts and 07-higher-dim): Surplus instead defines the tableau row's nonbasic quantities directly as the slack expression $s_j := (\tilde Ax)_j - \tilde b_j$, a genuine affine function of $x$ for every row, which reduces to $x_j$ itself exactly when row $j$ is that bound constraint — mathematically equivalent to the book's own substitution, stated without needing the row-to-variable lookup. Eq. (8.10)'s "$j\in J\cap N'$" strengthening-eligibility test has the same gap; this mission takes the row-positions eligible for strengthening as an explicit Finset parameter rather than deriving membership from row identity.

Corollary 8.6 is out of scope for this mission — see HARD.md. Its facet-counting bound depends on the same row/variable identification (the printed bound is $\binom{m+p+n-1}{n}$, excluding row $k$ specifically because it is $x_k$'s own bound row) and would additionally require a general notion of "number of facets of a polyhedron" that this mission's abstraction, and Mathlib, do not provide; it does not feed Theorem 8.7's own proof, which cites only Theorems 8.4A/8.4B and 8.5.

Theorem 8.7 is stated via one generic HasRankAtMost predicate applied to SplitConvexify (part a) and three closure operators (SimpleDisjClosureOfSet, StrengthenedLPClosureOfSet, MIGClosureOfSet, parts b-d) defined by intersecting a represented polyhedron with every cut of the corresponding family, then lifted to bare sets by quantifying over every linear representation — since, unlike the split-convexification closure, these three cut families are defined via an explicit basis or CGLP solution and so genuinely need some concrete representation of the current polyhedron at each step of the recursion (the same representation-dependence Theorem 7.5's Lovász-Schrijver iteration required in 07-higher-dim).

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 8.
• E. Balas, M. Perregaard, A precise correspondence between lift-and-project cuts, simple disjunctive cuts, and mixed integer Gomory cuts for 0-1 programming, Mathematical Programming B 94 (2003), 221–245 (cited in the text as [33], the origin of Lemma 8.2 and Theorems 8.4A/8.4B).
• E. Balas, M. Perregaard, Lift-and-project for mixed 0-1 programming: recent progress, Discrete Applied Mathematics 123 (2002), 129–154 (cited in the text as [32], the origin of Theorem 8.5's strengthened-cut coefficient identification).
• F. Eisenbrand, A. Schulz, Bounds on the Chvátal rank of polytopes in the 0-1 cube, in Integer Programming and Combinatorial Optimization (IPCO 7), LNCS 1610 (1999), 137–150 (cited in the text as [73], the source of the unbounded pure-integer Gomory rank result this chapter's Theorem 8.7 contrasts with).