Equivalent characterizations of $n$ linearly independent active constraints

Proved

LinearOptimization.lp_active_constraint_equiv

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

geometrylinear-programmingpolyhedra

(Theorem 2.2) Let $x^*$ be an element of $\mathbb{R}^n$ and let $I = \{i \mid a_i'x^* = b_i\}$ be the set of indices of constraints that are active at $x^*$ . Then, the following are equivalent:

(a) There exist $n$ vectors in the set $\{a_i \mid i \in I\}$ , which are linearly independent.
(b) The span of the vectors $a_i$ , $i \in I$ , is all of $\mathbb{R}^n$ , that is, every element of $\mathbb{R}^n$ can be expressed as a linear combination of the vectors $a_i$ , $i \in I$ .
(c) The system of equations $a_i'x = b_i$ , $i \in I$ , has a unique solution.

Preamble

import Mathlib.LinearAlgebra.LinearIndependent.Defs
import Mathlib.Data.List.TFAE
import Definitions.Def_ActiveConstraints


open Matrix

/-- **B&T Theorem 2.2 (p. 48).** Equivalent characterizations of "there are
`n` linearly independent constraints active at `x*`". In (c), `x*` itself
solves the active system, so uniqueness is stated as "every solution equals
`x*`". -/

Formal statement

theorem LinearOptimization.lp_active_constraint_equiv {ι : Type} [Fintype ι] {n : ℕ}
    (C : ι → LinearConstraint n) (x' : Fin n → ℝ) :
    List.TFAE
      [ ∃ s : Finset ι, s.card = n ∧ (∀ i ∈ s, (C i).IsActiveAt x') ∧
          LinearIndependent ℝ (fun i : s => (C i.1).a),
        Submodule.span ℝ ((fun i => (C i).a) '' {i | (C i).IsActiveAt x'}) = ⊤,
        ∀ y : Fin n → ℝ,
          (∀ i, (C i).IsActiveAt x' → (C i).a ⬝ᵥ y = (C i).b) → y = x' ] := by
  sorry

Source

Bertsimas & Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.2, p. 48

Read-back

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

Let $\iota$ be a finite type, $C : \iota \to$ linear constraints on $\mathbb{R}^n$ (each $C_i$ has coefficient vector $a_i$ , right-hand side $b_i$ , and a $\ge$ / $\le$ / $=$ tag; "active at $x$ " means $a_i \cdot x = b_i$ regardless of tag), and let $x' \in \mathbb{R}^n$ be arbitrary — it is not assumed to satisfy any constraint. The theorem asserts that the following three statements are pairwise equivalent: (1) there exists a finite set $s \subseteq \iota$ of cardinality exactly $n$ such that every constraint in $s$ is active at $x'$ and the vectors $(a_i)_{i \in s}$ are linearly independent over $\mathbb{R}$ ; (2) the linear span of the set of vectors $\{a_i \mid C_i \text{ active at } x'\}$ is all of $\mathbb{R}^n$ ; (3) $x'$ is the unique solution of the active equations: every $y \in \mathbb{R}^n$ satisfying $a_i \cdot y = b_i$ for every index $i$ whose constraint is active at $x'$ must equal $x'$ . Edge cases silently included: when $n = 0$ all three are trivially true; when no constraint is active at $x'$ , (2) demands $\mathrm{span}(\varnothing) = \mathbb{R}^n$ and (3) demands that all of $\mathbb{R}^n$ equals $\{x'\}$ .

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

Equivalent characterizations of nnn linearly independent active constraints

Equivalent characterizations of $n$ linearly independent active constraints