Optimality criterion — a tableau with $r \le 0$ gives an optimal basic feasible solution

Proved

MatousekLP.Simplex.optimality_criterion

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

linear-programmingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1simplex-method

Let $A$ be a real $m\times n$ matrix of rank $m$ with $n\ge m$ , $b\in\mathbb{R}^m$ , $c\in\mathbb{R}^n$ , and let $B$ be a feasible basis of "maximize $c^Tx$ subject to $Ax=b$ , $x\ge0$ ". Let $r=c_N-(c_B^TA_B^{-1}A_N)^T$ be the last row of its simplex tableau $T(B)$ . If

r\le 0,

then the basic feasible solution of $B$ (the $x$ with $Ax=b$ and $x_j=0$ for all $j\notin B$ ) is an optimal solution.

This is the stopping test of the simplex method: when no nonbasic variable has a positive coefficient in the objective row, the current basic feasible solution is optimal.

Formalization Note Indices are 0-based. The basic feasible solution is described by the two properties that determine it ( $Ax=b$ , zero outside $B$ ). Optimality is stated against every feasible solution; no supremum is used. The standing assumption of §4.2 is a hypothesis.

Preamble

import Mathlib
import Definitions.Def_MatousekLP_Simplex_Tableau
open Matrix Filter

Formal statement

namespace MatousekLP.Simplex

/-- Optimality criterion (§5.6, p. 67, boxed). If `B` is a feasible basis and the last row of
the simplex tableau `T(B)` has `r ≤ 0`, then the basic feasible solution of `B` is optimal.
Standing assumption of §4.2 (p. 44): `n ≥ m` and `A` has rank `m`. -/
theorem optimality_criterion {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (c : Fin n → ℝ) (hmn : m ≤ n) (hrank : A.rank = m) (B : Finset (Fin n)) (hB : B.card = m)
    (hfeas : IsFeasibleBasisOf A b B hB) (hr : tableauR A c B hB ≤ 0) (x : Fin n → ℝ)
    (hx : IsBasicSolutionFor A b B x) :
    MatousekLP.BFS.IsOptimal A b c x := by sorry

end MatousekLP.Simplex

Source

Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, §5.6, p. 67, optimality criterion (boxed, unnumbered)

Human review

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

View graph

Optimality criterion — a tableau with r≤0r \le 0r≤0 gives an optimal basic feasible solution

Optimality criterion — a tableau with $r \le 0$ gives an optimal basic feasible solution