EconCSLib.Math.LinearProgramming.StrongComplementarity

Formalises LP strong complementary slackness [MFoGT, Section 2.8, Exercise 11] over any linearly ordered field.

For the standard-form primal/dual pair

Primal P: min ⟨c, x⟩ subject to A x ≥ b and x ≥ 0 Dual D: max ⟨u, b⟩ subject to uᵀ A ≤ c and u ≥ 0

if both are feasible, then there exist optimal x and u such that

(Ax − b)_i > 0 ⟺ u_i = 0, for every row i, (c − uᵀA)_j > 0 ⟺ x_j = 0, for every column j.

That is, for every complementary pair (primal slack on row i, dual variable u_i; resp. dual slack on column j, primal variable x_j), exactly one of the two is strictly positive in some optimal pair.

Proof strategy

The hard direction (strong content) follows from LP strong duality applied to a perturbed LP, then combined across all constraints by convex aggregation. The easy direction is weak complementary slackness, which is a direct consequence of any optimal pair.

This file proves:

• lp_weak_complementarity — the easy direction (strict slack ⇒ zero variable), holds for every optimal primal-dual pair.
• exists_lp_strong_complementarity — the existence form of the full bidirectional strong complementarity.

Blueprint

• docs/knowledge/nodes/core/linear_programming.strong_complementarity.md

Weak complementary slackness

For any optimal primal-dual pair (x, u) with matching objective values, the standard CS identities hold:

(Ax − b)_i · u_i = 0 for every row i, (c − uᵀA)_j · x_j = 0 for every column j.

Equivalently: strict primal slack forces the corresponding dual variable to vanish, and strict dual slack forces the corresponding primal variable to vanish.

theorem EconCSLib.LinearProgramming.lp_weak_complementarity_row {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) {x : Fin n → 𝕜} (hxA : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) (hxnn : ∀ (j : Fin n), 0 ≤ x j) {u : I → 𝕜} (hu_du : DualFeasible A c u) (h_match : ∑ j : Fin n, c j * x j = ∑ i : I, u i * b i) (i : I) : (∑ j : Fin n, A i j * x j - b i) * u i = 0

Weak complementary slackness, row form.

theorem EconCSLib.LinearProgramming.lp_weak_complementarity_col {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) {x : Fin n → 𝕜} (hxA : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) (hxnn : ∀ (j : Fin n), 0 ≤ x j) {u : I → 𝕜} (hu_du : DualFeasible A c u) (h_match : ∑ j : Fin n, c j * x j = ∑ i : I, u i * b i) (j : Fin n) : (c j - ∑ i : I, u i * A i j) * x j = 0

Weak complementary slackness, column form.

Optimality-augmented system

For the per-index strong-CS dichotomy we apply Farkas to the system encoding "primal-optimal x": A x ≥ b, x ≥ 0, ⟨c, x⟩ ≤ v. The augmented row index is (I ⊕ Fin n) ⊕ Unit:

• inl (inl i) ↦ original row A i x ≥ b i,
• inl (inr j') ↦ unit row x_{j'} ≥ 0,
• inr () ↦ optimality row -⟨c, x⟩ ≥ -v (i.e. ⟨c, x⟩ ≤ v).

@[reducible, inline]

abbrev EconCSLib.LinearProgramming.OptAugRow (I : Type u_3) (n : ℕ) : Type u_3

Optimality-augmented row index.

Equations

• EconCSLib.LinearProgramming.OptAugRow I n = ((I ⊕ Fin n) ⊕ Unit)

def EconCSLib.LinearProgramming.optAugA {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) : OptAugRow I n → Fin n → 𝕜

Optimality-augmented matrix.

Equations

• EconCSLib.LinearProgramming.optAugA A c (Sum.inl (Sum.inl i)) x✝ = A i x✝
• EconCSLib.LinearProgramming.optAugA A c (Sum.inl (Sum.inr j')) x✝ = if x✝ = j' then 1 else 0
• EconCSLib.LinearProgramming.optAugA A c (Sum.inr PUnit.unit) x✝ = -c x✝

def EconCSLib.LinearProgramming.optAugB {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (b : I → 𝕜) (v : 𝕜) : OptAugRow I n → 𝕜

Optimality-augmented RHS.

Equations

• EconCSLib.LinearProgramming.optAugB b v (Sum.inl (Sum.inl i)) = b i
• EconCSLib.LinearProgramming.optAugB b v (Sum.inl (Sum.inr val)) = 0
• EconCSLib.LinearProgramming.optAugB b v (Sum.inr PUnit.unit) = -v

@[simp]

theorem EconCSLib.LinearProgramming.optAugA_inl_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) (i : I) (j : Fin n) : optAugA A c (Sum.inl (Sum.inl i)) j = A i j

@[simp]

theorem EconCSLib.LinearProgramming.optAugA_inl_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) (j' j : Fin n) : optAugA A c (Sum.inl (Sum.inr j')) j = if j = j' then 1 else 0

@[simp]

theorem EconCSLib.LinearProgramming.optAugA_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) (j : Fin n) : optAugA A c (Sum.inr ()) j = -c j

@[simp]

theorem EconCSLib.LinearProgramming.optAugB_inl_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (b : I → 𝕜) (v : 𝕜) (i : I) : optAugB b v (Sum.inl (Sum.inl i)) = b i

@[simp]

theorem EconCSLib.LinearProgramming.optAugB_inl_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (b : I → 𝕜) (v : 𝕜) (j' : Fin n) : optAugB b v (Sum.inl (Sum.inr j')) = 0

@[simp]

theorem EconCSLib.LinearProgramming.optAugB_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (b : I → 𝕜) (v : 𝕜) : optAugB b v (Sum.inr ()) = -v

theorem EconCSLib.LinearProgramming.optAug_feasible_iff {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (v : 𝕜) (x : Fin n → 𝕜) : (∀ (idx : OptAugRow I n), optAugB b v idx ≤ ∑ j : Fin n, optAugA A c idx j * x j) ↔ (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) ∧ (∀ (j : Fin n), 0 ≤ x j) ∧ ∑ j : Fin n, c j * x j ≤ v

An x satisfies optAugA · x ≥ optAugB iff x is primal-feasible and has objective at most v.

Per-row dichotomy

For each fixed row i₀, there exists an optimal primal-dual pair (x, u) with the row complementarity sum (Ax - b)_{i₀} + u_{i₀} strictly positive.

This is the key step that upgrades weak CS to strong CS at one specific row. The proof is by classical case analysis:

• Case A: some primal-optimal x has (Ax - b)_{i₀} > 0. Pair with any dual-optimal u.
• Case B: every primal-optimal x has (Ax - b)_{i₀} = 0. Apply Farkas to the bound implication (Ax - b)_{i₀} ≤ 0 on the augmented system; the certificate yields a dual-optimal u with u_{i₀} > 0.

theorem EconCSLib.LinearProgramming.exists_row_strict_pair {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (v : 𝕜) {x₀ : Fin n → 𝕜} (hx₀A : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x₀ j) (hx₀nn : ∀ (j : Fin n), 0 ≤ x₀ j) (hx₀_val : ∑ j : Fin n, c j * x₀ j = v) {u₀ : I → 𝕜} (hu₀ : DualFeasible A c u₀) (hu₀_val : ∑ i : I, u₀ i * b i = v) (i₀ : I) : ∃ (x : Fin n → 𝕜) (u : I → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) ∧ (∀ (j : Fin n), 0 ≤ x j) ∧ DualFeasible A c u ∧ ∑ j : Fin n, c j * x j = v ∧ ∑ i : I, u i * b i = v ∧ 0 < ∑ j : Fin n, A i₀ j * x j - b i₀ + u i₀

Per-row strict-CS witness: for each row i₀, there exists an optimal primal-dual pair with (Ax - b)_{i₀} + u_{i₀} > 0.

Hypotheses:

• hx₀ — x₀ is primal-feasible with ⟨c, x₀⟩ = v (primal-optimal).
• hu₀ — u₀ is dual-feasible with ⟨u₀, b⟩ = v (dual-optimal).

Both x₀ and u₀ exist by LP strong duality when both P and D are feasible.

Per-column dichotomy

For each fixed column j₀, there exists an optimal primal-dual pair (x, u) with the column complementarity sum x_{j₀} + (c - uᵀA)_{j₀} strictly positive.

We reuse the primal augmented system optAugA/optAugB (so the variable type stays Fin n as required by farkas_lemma), with cost vector -e_{j₀} on the primal-feasibility set:

• Case A: some primal-optimal x has x_{j₀} > 0. Pair with any dual-optimal u.
• Case B: every primal-optimal x has x_{j₀} = 0. Apply Farkas to the bound implication -x_{j₀} ≥ 0 on the augmented system; the certificate yields a dual-optimal u with (c - uᵀA)_{j₀} > 0.

theorem EconCSLib.LinearProgramming.exists_col_strict_pair {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (v : 𝕜) {x₀ : Fin n → 𝕜} (hx₀A : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x₀ j) (hx₀nn : ∀ (j : Fin n), 0 ≤ x₀ j) (hx₀_val : ∑ j : Fin n, c j * x₀ j = v) {u₀ : I → 𝕜} (hu₀ : DualFeasible A c u₀) (hu₀_val : ∑ i : I, u₀ i * b i = v) (j₀ : Fin n) : ∃ (x : Fin n → 𝕜) (u : I → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) ∧ (∀ (j : Fin n), 0 ≤ x j) ∧ DualFeasible A c u ∧ ∑ j : Fin n, c j * x j = v ∧ ∑ i : I, u i * b i = v ∧ 0 < x j₀ + (c j₀ - ∑ i : I, u i * A i j₀)

Per-column strict-CS witness: for each column j₀, there exists an optimal primal-dual pair with x_{j₀} + (c - uᵀA)_{j₀} > 0.

Strong complementarity: main theorem

Given an optimal primal-dual pair (x₀, u₀) with common value v, the per-index dichotomies produce Fintype.card I + n witness pairs, one strict at each row and each column. Convex combination (averaging) preserves optimality and gives a single pair strict at every index.

theorem EconCSLib.LinearProgramming.exists_strong_complementary_pair {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (v : 𝕜) (hN_pos : 0 < ↑(Fintype.card I + n)) {x₀ : Fin n → 𝕜} (hx₀A : ∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x₀ j) (hx₀nn : ∀ (j : Fin n), 0 ≤ x₀ j) (hx₀_val : ∑ j : Fin n, c j * x₀ j = v) {u₀ : I → 𝕜} (hu₀ : DualFeasible A c u₀) (hu₀_val : ∑ i : I, u₀ i * b i = v) : ∃ (x : Fin n → 𝕜) (u : I → 𝕜), (∀ (i : I), b i ≤ ∑ j : Fin n, A i j * x j) ∧ (∀ (j : Fin n), 0 ≤ x j) ∧ DualFeasible A c u ∧ ∑ j : Fin n, c j * x j = v ∧ ∑ i : I, u i * b i = v ∧ (∀ (i : I), 0 < ∑ j : Fin n, A i j * x j - b i + u i) ∧ ∀ (j : Fin n), 0 < x j + (c j - ∑ i : I, u i * A i j)

LP Strong Complementarity [MFoGT, Section 2.8, Exercise 11]: given an optimal primal-dual pair (x₀, u₀) with common value v, there exists an optimal pair (x*, u*) such that for every row i ∈ I and column j ∈ Fin n, the row complementarity sum (Ax* - b)_i + u*_i and the column complementarity sum x*_j + (c - u*ᵀA)_j are strictly positive. Combined with weak complementary slackness, this is the strict biconditional form.