Khachiyan's theorem: LP feasibility in polynomially many ellipsoid iterations

Proved

SmaleNinth.khachiyan_ellipsoid_decides

by ORdos · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-complexityellipsoid-methodkhachiyanlinear-programmingpolynomial-time

This is the statement that linear feasibility with integer data is decided in polynomially many ellipsoid iterations — the 1979 result that placed linear programming in polynomial time.

The iteration. An admissible run of the ellipsoid method on a system $Cx \ge d$ is a sequence of centres $x_t \in \mathbb{R}^n$ and shape matrices $D_t$ such that, at every time $t$ at which the current centre is infeasible, some violated row $c_i^{\mathsf T} x_t < d_i$ is selected and the successor is produced by the standard update

x_{t+1} = x_t + \frac{1}{n+1}\cdot\frac{D_t c_i}{\sqrt{c_i^{\mathsf T} D_t c_i}}, \qquad D_{t+1} = \frac{n^2}{n^2-1}\left(D_t - \frac{2}{n+1}\cdot\frac{D_t c_i c_i^{\mathsf T} D_t}{c_i^{\mathsf T} D_t c_i}\right),

the smallest ellipsoid containing the half of the current one that still contains the feasible set. Nothing constrains which violated row is chosen, so the theorem holds for every rule for selecting violated constraints; and nothing is constrained once a centre is feasible, since the algorithm has then answered.

The assertion. Let $n \ge 2$ and $U \ge 1$ , let $A \in \mathbb{Z}^{m\times n}$ and $b \in \mathbb{Z}^m$ have entries bounded by $U$ in absolute value, and consider any admissible run on the perturbed-and-boxed system $\widehat P$ started at $x_0 = 0$ with $D_0 = r^2 I$ , the ball of enclosing radius $r = (n+1)(n!\,U^n+1)$ . Then

\bigl(\exists\, t \le t^{*} :\ x_t \in \widehat P\bigr) \qquad\Longleftrightarrow\qquad \{x \in \mathbb{R}^n \mid Ax \ge b\} \ne \emptyset ,

and the budget is polynomially bounded,

t^{*} \;\le\; 10^{6}\,(n+2)^{4}\,\bigl(\log_2 U + n + 2\bigr).

Reading the equivalence. The two sides concern different sets: the run is observed on the perturbed-and-boxed system, while the conclusion is about the original system. That the one decides the other is the content of the perturbation bounds. Running the budget to exhaustion without a feasible centre is therefore a proof of infeasibility, not merely a failure to find a point.

Where the hypotheses bite. The restriction $n \ge 2$ comes from the factor $n^2/(n^2-1)$ in the update, and $U \ge 1$ keeps the constants nondegenerate. The numerical bound uses the integer base- $2$ logarithm, and its constant is deliberately generous — only the polynomial order in $n$ and $\log U$ is load-bearing.

What remains open after this. The count is polynomial in $n$ and in $\log U$ , the bit length of the data. Removing that dependence on $U$ — a bound in $m$ and $n$ alone, valid for arbitrary real data — is exactly the mission's goal, and no known method achieves it.

Preamble

import Definitions.Def_Polyhedron
import Definitions.Def_LinearOptimization_Ellipsoid
import Definitions.Def_LinearOptimization_EllipsoidMethod
import Definitions.Def_SmaleNinth_Khachiyan

/-!
Khachiyan's theorem in iteration form: the ellipsoid method decides the
feasibility of an integer linear system within an explicitly polynomial
number of iterations.

Source: L.G. Khachiyan, *A polynomial algorithm in linear programming*,
Soviet Math. Doklady 20 (1979) 191–194 — the result that linear programming
feasibility with rational data is decidable in polynomial time. Textbook
treatment: B. Korte, J. Vygen, *Combinatorial Optimization*, 6th ed.,
§4.4–4.5 (Khachiyan's theorem); the ellipsoid iteration itself is the
platform's `LinearOptimization` development of Bertsimas–Tsitsiklis,
*Introduction to Linear Optimization*, Chapter 8.

Every admissible run of the ellipsoid method (any rule for choosing violated
constraints) on the perturbed-and-boxed system, started from the ball of
radius `khachiyanRadius n U`, decides within `khachiyanIterations n U`
iterations whether `Ax ≥ b` is solvable: some center lands in the
perturbed-and-boxed polyhedron iff the original system is solvable. The
iteration budget is bounded by an explicit polynomial in `n` and `log₂ U` —
this, not any particular constant, is the content of "polynomially many
iterations". (The generous constant `10⁶·(n+2)⁴·(log₂ U + n + 2)` absorbs
the crude Cramer–Hadamard estimates fixed in
`Definitions.Def_SmaleNinth_Khachiyan`.)
-/

open Matrix LinearOptimization

/-- **Khachiyan's theorem, iteration form** (Khachiyan 1979; Korte–Vygen
§4.5). For an integer system `Ax ≥ b` in `n ≥ 2` variables with entries
bounded by `U ≥ 1`: every admissible ellipsoid run on the
perturbed-and-boxed system, started at the origin with the ball of radius
`khachiyanRadius n U`, hits the perturbed-and-boxed polyhedron with some
center within `khachiyanIterations n U` iterations **iff** `Ax ≥ b` has a
real solution — and the iteration budget is polynomially bounded:
`khachiyanIterations n U ≤ 10⁶·(n+2)⁴·(log₂ U + n + 2)`. -/

Formal statement

theorem SmaleNinth.khachiyan_ellipsoid_decides {m n : ℕ} (U : ℕ) (hU : 1 ≤ U)
    (hn : 2 ≤ n) (A : Matrix (Fin m) (Fin n) ℤ) (b : Fin m → ℤ)
    (hA : ∀ i j, |A i j| ≤ (U : ℤ)) (hb : ∀ i, |b i| ≤ (U : ℤ))
    (x : ℕ → Fin n → ℝ) (D : ℕ → Matrix (Fin n) (Fin n) ℝ)
    (hx0 : x 0 = 0)
    (hD0 : D 0 = (khachiyanRadius n U) ^ 2 • (1 : Matrix (Fin n) (Fin n) ℝ))
    (hrun : IsEllipsoidRun (khachiyanSystemA A) (khachiyanSystemb n U b)
      x D (khachiyanIterations n U)) :
    ((∃ t ≤ khachiyanIterations n U,
        x t ∈ polyhedron (khachiyanSystemA A) (khachiyanSystemb n U b)) ↔
      (polyhedron (A.map (Int.cast : ℤ → ℝ))
        (fun i => (b i : ℝ))).Nonempty) ∧
    khachiyanIterations n U ≤
      10 ^ 6 * (n + 2) ^ 4 * (Nat.log 2 U + n + 2) := by sorry

Source

L.G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979) 191-194. Textbook: B. Korte, J. Vygen, Combinatorial Optimization, 6th ed., Section 4.5 (Khachiyan's theorem); ellipsoid iteration harness: Bertsimas-Tsitsiklis, Introduction to Linear Optimization, Chapter 8 (platform mission Introduction to Linear Optimization XI).

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `SmaleNinth.khachiyan_ellipsoid_decides`

Setting and hypotheses. The theorem is stated for arbitrary natural numbers $m$ and $n$ (both implicit; $m = 0$ , i.e. a system with no constraint rows, is allowed) and a natural number $U$ , under the hypotheses $U \ge 1$ and $n \ge 2$ . It takes an integer $m \times n$ matrix $A$ and an integer vector $b \in \mathbb{Z}^m$ with every entry bounded: $|A_{ij}| \le U$ for all $i, j$ , and $|b_i| \le U$ for all $i$ . It also takes two infinite sequences indexed by all natural numbers $t = 0, 1, 2, \dots$ : a sequence of centers $x_t \in \mathbb{R}^n$ and a sequence of $n \times n$ real matrices $D_t$ (with no symmetry or positive-definiteness assumption placed on any $D_t$ ).

Fixed constants. The statement uses the following explicitly defined quantities (all functions of $n$ and $U$ only):

\varepsilon = \frac{1}{2\,(n+1)\,(n+1)!\,U^{\,n+1}}, \qquad M = n!\,U^{\,n} + 1, \qquad r = (n+1)\,M,

v = \left(\frac{\varepsilon}{nU}\right)^{\!n}, \qquad T = \left\lceil 2(n+1)\,\ln\!\frac{(2r)^n}{v/2} \right\rceil,

where $\ln$ is the natural logarithm and $\lceil \cdot \rceil$ here is the ceiling into the natural numbers (a negative or undefined argument would be sent to $0$ ; the Lean logarithm is total, with $\ln$ of a nonpositive number equal to $0$ ). The theorem calls $T$ the iteration budget ("khachiyanIterations").

The perturbed-and-boxed system. From $A$ and $b$ the statement builds a real system with $m + 2n$ rows in $n$ variables: a matrix $A'$ whose first $m$ rows are the rows of $A$ (cast to $\mathbb{R}$ ), whose next $n$ rows are the $n \times n$ identity, and whose last $n$ rows are minus the identity; and a right-hand side $b'$ equal to $b_i - \varepsilon$ on the first $m$ rows and to $-M$ on all $2n$ remaining rows. The associated polyhedron — throughout, "polyhedron of $(C, d)$ " means the set $\{x \in \mathbb{R}^n \mid Cx \ge d \text{ componentwise}\}$ — is therefore

P' \;=\; \{\, x \in \mathbb{R}^n \;\mid\; Ax \ge b - \varepsilon \mathbf{1} \ \text{ and } \ -M \le x_j \le M \ \text{for all } j \,\}.

Initial conditions. The hypotheses fix $x_0 = 0$ (the origin) and $D_0 = r^2 I$ , the shape matrix of the ball of radius $r$ centered at the origin.

The run hypothesis, unfolded. The remaining hypothesis is that $(x_t, D_t)$ is an "ellipsoid run" on $(A', b')$ up to time $T$ , which literally means: for every $t < T$ such that $x_t \notin P'$ , there exists some row index $i$ of the stacked system (any row among the $m + 2n$ ) whose constraint is violated strictly at $x_t$ , i.e. $a_i^{\mathsf T} x_t < b'_i$ where $a_i$ is the $i$ -th row of $A'$ , and such that the next iterate is exactly the ellipsoid update with respect to that row:

x_{t+1} = x_t + \frac{1}{n+1}\,\frac{D_t\,a_i}{\sqrt{a_i^{\mathsf T} D_t\, a_i}}, \qquad D_{t+1} = \frac{n^2}{n^2 - 1}\left( D_t - \frac{2}{n+1}\,\frac{D_t\, a_i\, a_i^{\mathsf T} D_t}{a_i^{\mathsf T} D_t\, a_i} \right).

(These formulas are Lean-total: the square root of a negative number is $0$ and the inverse of $0$ is $0$ , so the equations are meaningful — with junk values — even when $a_i^{\mathsf T} D_t a_i \le 0$ ; nothing in the hypothesis requires it to be positive.) This is the entire content of the run hypothesis. In particular: it constrains nothing at any time $t < T$ at which $x_t \in P'$ (at such $t$ the pair $(x_{t+1}, D_{t+1})$ is completely arbitrary, so the sequences after a "hit" are unconstrained); it constrains nothing at times $t \ge T$ ; it does not specify which violated row is used (any choice rule is admissible); and it never asserts that the algorithm stops — the sequences are given for all time. When $x_t \notin P'$ some violated row necessarily exists, so the existence part of the condition is never vacuously impossible; the hypothesis is a genuine constraint only in that the update must use some strictly violated row's formulas.

Conclusion. Under all the above, the theorem asserts the conjunction of two claims:

(Decision, as an iff.) There exists a time $t$ with $0 \le t \le T$ (the bound is inclusive, so $t = T$ and $t = 0$ both count) such that $x_t \in P'$ — i.e. some center of the run lands in the perturbed-and-boxed polyhedron within the budget — if and only if the polyhedron of the original system over the reals, $\{ x \in \mathbb{R}^n \mid Ax \ge b \}$ (with $A, b$ cast from $\mathbb{Z}$ to $\mathbb{R}$ , no perturbation and no box), is nonempty.
(Budget bound.) The iteration budget satisfies the numerical inequality

T \;\le\; 10^6 \,(n+2)^4\,\bigl(\lfloor \log_2 U \rfloor + n + 2\bigr),

where $\lfloor \log_2 U \rfloor$ is the natural-number base-2 logarithm of $U$ (the largest $k$ with $2^k \le U$ ; it equals $0$ for $U = 1$ ), and the inequality is between natural numbers.

Note that the iff in claim 1 relates membership in the perturbed-and-boxed set $P'$ (not the original polyhedron) to nonemptiness of the original set; the two sides concern different polyhedra. Also, claim 2 is a purely numerical statement about $n$ and $U$ and does not involve the run, but it is asserted only under all of the theorem's hypotheses, including the existence of the given run.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by ORdos · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Khachiyan's theorem: LP feasibility in polynomially many ellipsoid iterations

Read-back: SmaleNinth.khachiyan_ellipsoid_decides

Read-back: `SmaleNinth.khachiyan_ellipsoid_decides`