Finite termination of the simplex method under nondegeneracy

Proved

LinearOptimization.simplex_termination_nondegenerate

by Shuze Chen · 1 vote · Aug 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-programmingoptimalitysimplextermination

(Theorem 3.3, GOAL) Assume that the feasible set is nonempty and that every basic feasible solution is nondegenerate. Then, the simplex method terminates after a finite number of iterations. At termination, there are the following two possibilities:

(a) we have an optimal basis $B$ and an associated basic feasible solution which is optimal;
(b) we have found a vector $d$ satisfying $Ad = 0$ , $d \ge 0$ , and $c'd < 0$ , and the optimal cost is $-\infty$ .

Encoding: (Termination is encoded as: there is no infinite admissible pivot run, and every maximal run ends in one of the two terminal states.)

Preamble

import Mathlib.LinearAlgebra.LinearIndependent.Defs
import Definitions.Def_LinearOptimization_SimplexPivot
import Definitions.Def_LinearOptimization_OptimalBasis


open Matrix

/-- **Bertsimas & Tsitsiklis, Theorem 3.3 (p. 91).** Termination of the simplex method under
nondegeneracy: if the standard-form feasible set is nonempty and every
basic feasible solution is nondegenerate, then no infinite pivot run
exists, and every admissible state admitting no further pivot exhibits
either an optimal basis with an optimal associated basic feasible
solution, or a direction `d` with `Ad = 0`, `d ≥ 0`, `c'd < 0`
certifying optimal cost `−∞`. -/

Formal statement

theorem LinearOptimization.simplex_termination_nondegenerate {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ)
    (hA : LinearIndependent ℝ (fun i => A i))
    (hne : (stdPolyhedron A b).Nonempty)
    (hnd : ∀ x, IsBasicFeasibleSolution (stdFormSystem A b) x →
      ¬IsStdDegenerateBasicSolution A b x) :
    (¬∃ f : ℕ → (Fin m ↪ Fin n) × (Fin n → ℝ),
      (∀ k, IsSimplexState A b (f k).1 (f k).2) ∧
      ∀ k, IsSimplexPivot A c (f k).1 (f k).2 (f (k + 1)).1 (f (k + 1)).2) ∧
    ∀ (B : Fin m ↪ Fin n) (x : Fin n → ℝ), IsSimplexState A b B x →
      (¬∃ (B' : Fin m ↪ Fin n) (x' : Fin n → ℝ), IsSimplexPivot A c B x B' x') →
      (IsOptimalBasis A b c B ∧ IsLpOptimal c (stdPolyhedron A b) x) ∨
      ∃ d : Fin n → ℝ, A.mulVec d = 0 ∧ 0 ≤ d ∧ c ⬝ᵥ d < 0 ∧
        lpValue c (stdPolyhedron A b) = ⊥ := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 3.3, p. 91

Read-back

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

Let $A$ be a real $m \times n$ matrix with linearly independent rows, $b \in \mathbb{R}^m$ , $c \in \mathbb{R}^n$ . Assume the standard polyhedron $S = \{x \mid Ax = b, x \ge 0\}$ is nonempty and that every basic feasible solution of the standard-form constraint system is not std-degenerate (never both a basic solution and with more than $n \dot- m$ zero coordinates). The conclusion is a conjunction. (a) There is no infinite sequence $(B_k, x_k)_{k \in \mathbb{N}}$ in which every $(B_k, x_k)$ is a simplex state (basis columns independent, $x_k \in S$ , nonbasic coordinates zero) and every consecutive pair is related by a simplex pivot (an entering nonbasic column with negative reduced cost, a leaving row with positive pivot-column entry attaining the minimum ratio, and the update $x_{k+1} = x_k + \theta^* d$ ). (b) For every simplex state $(B, x)$ from which no simplex pivot to any $(B', x')$ exists, either ( $B$ is an optimal basis: independent columns, $A_B^{-1}b \ge 0$ , all reduced costs $\ge 0$ — and $x$ minimizes $c \cdot y$ over $S$ ), or there exists $d \in \mathbb{R}^n$ with $Ad = 0$ , $d \ge 0$ , $c \cdot d < 0$ , and $\inf_{y \in S} c \cdot y = -\infty$ in the extended reals. Note (a) rules out infinite pivot sequences of any kind under the global non-degeneracy hypothesis, and in (b) the no-pivot condition is over the specific pivot relation defined in the bundle.

Human review

Endorsed by Community (Bot) · Aug 5, 2026
Endorsed by Shuze Chen · Aug 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph