Basic solutions of standard-form polyhedra via basis columns

Proved

LinearOptimization.lp_standard_form_basic_iff

by Shuze Chen · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-programmingpolyhedrasimplex

(Theorem 2.4) Consider the constraints $Ax = b$ and $x \ge 0$ and assume that the $m \times n$ matrix $A$ has linearly independent rows. A vector $x \in \mathbb{R}^n$ is a basic solution if and only if we have $Ax = b$ , and there exist indices $B(1), \dots, B(m)$ such that:

(a) The columns $A_{B(1)}, \dots, A_{B(m)}$ are linearly independent;
(b) If $i \ne B(1), \dots, B(m)$ , then $x_i = 0$ .

Preamble

import Mathlib.LinearAlgebra.LinearIndependent.Defs
import Definitions.Def_BasicSolution


open Matrix

/-- **B&T Theorem 2.4 (p. 53).** Characterization of basic solutions of the
standard-form system: under the book's explicit hypothesis that the rows of
`A` are linearly independent, `x` is a basic solution iff `Ax = b` and the
nonzero coordinates of `x` live inside some basis `B` (injective basic
indices with linearly independent basic columns). -/

Formal statement

theorem LinearOptimization.lp_standard_form_basic_iff {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (b : Fin m → ℝ) (hA : LinearIndependent ℝ (fun i => A i))
    (x : Fin n → ℝ) :
    IsBasicSolution (stdFormSystem A b) x ↔
      A.mulVec x = b ∧ ∃ B : Fin m ↪ Fin n, IsStdBasis A B ∧
        ∀ j, j ∉ Set.range B → x j = 0 := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.4, p. 53

Read-back

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

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ , and assume the rows of $A$ (the family $i \mapsto A_i \in \mathbb{R}^n$ ) are linearly independent over $\mathbb{R}$ (this forces $m \le n$ and, when $m \ge 1$ , excludes zero rows and repeated rows). For any $x \in \mathbb{R}^n$ , the theorem asserts an if and only if: $x$ is a basic solution of the standard-form constraint system (the $m$ equality constraints $A_i \cdot x = b_i$ together with the $n$ sign constraints $x_j \ge 0$ ; "basic solution" means all equality constraints are active at $x$ and some $n$ -element set of constraints from the combined family is active at $x$ with linearly independent coefficient vectors) iff $Ax = b$ and there exists an injection $B : \{1..m\} \hookrightarrow \{1..n\}$ such that the $m$ columns of $A$ selected by $B$ are linearly independent and $x_j = 0$ for every column index $j$ outside the range of $B$ . Note the right-hand side does not assert $x \ge 0$ , and the sign constraints enter the left-hand side only through activity ( $x_j = 0$ ), not satisfaction.

Human review

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

View graph