Theorem 3.1 — a nonterminating simplex run must cycle

Open

VanderbeiLP.Simplex.nonterminating_implies_cycling

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

cyclinglinear-programmingp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1simplex-method

Consider a standard-form linear program with data $A \in \mathbb{R}^{m\times n}$ , $b\in\mathbb{R}^m$ , $c \in \mathbb{R}^n$ , and an infinite run of the simplex method: a sequence of dictionaries $D_0, D_1, D_2, \dots$ with $D_0$ feasible, in which each $D_{t+1}$ is obtained from $D_t$ by a simplex pivot (an entering candidate $x_k$ with $\bar c_k > 0$ and a leaving candidate chosen by the ratio test, by any rule). Then the run visits some dictionary more than once:

\exists\, s < t:\quad D_s = D_t .

This is the first step of the chapter's termination analysis: a variant of the simplex method terminates as soon as it is known never to cycle.

Formalization Note Dictionaries are identified with their basic sets, so $D_s = D_t$ means that the same variables are basic.

Preamble

import Mathlib
import Definitions.Def_VanderbeiLP_Simplex_Dictionary
import Definitions.Def_VanderbeiLP_Simplex_PivotRules

Formal statement

namespace VanderbeiLP.Simplex

/-- **Vanderbei, Theorem 3.1 (p. 27).** If the simplex method fails to terminate, then it must
cycle: an infinite run of simplex pivots (any choice of entering and leaving candidates at each
step) started at a feasible dictionary visits some dictionary more than once. -/
theorem nonterminating_implies_cycling {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (c : Fin n → ℝ) (D : ℕ → Dictionary A) (h0 : (D 0).IsFeasible b)
    (hstep : ∀ t, Dictionary.IsSimplexPivot b c (D t) (D (t + 1))) :
    ∃ s t, s < t ∧ D s = D t := by sorry

end VanderbeiLP.Simplex

Source

Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer 2014, p. 27 (PDF 44), Theorem 3.1

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph