EconCSLib.Math.LinearAlgebra.FourierMotzkin

Formalises the Theorem of the Alternative [MFoGT, Section 2.8, Exercise 7] over any linearly ordered field ([Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]). We prove the Fin m × Fin n version directly; a general Fintype I form would transport via Fintype.equivFin.

For a finite system of weak linear inequalities A x ≥ b with A : Fin m → Fin n → 𝕜, b : Fin m → 𝕜, exactly one of:

• the primal set S = { x : Fin n → 𝕜 | ∀ i, ⟨A i, x⟩ ≥ b i }, or
• the Farkas certificate set T = { u : Fin m → 𝕜 | u ≥ 0, uᵀA = 0, ⟨u, b⟩ > 0 }

is nonempty.

Blueprint

• docs/knowledge/nodes/core/linear_algebra.theorem_of_alternative.md
• docs/knowledge/nodes/core/linear_algebra.theorem_of_alternative.fourier_motzkin.md

The primal feasibility set and Farkas certificate set

We parameterise the row index by an abstract Fintype I (rather than Fin m) because the Fourier-Motzkin reduction produces a row index of the form I⁰ ⊕ (I⁺ × I⁻), which is naturally a Fintype but does not stay Fin m. A user typically instantiates I := Fin m at the application boundary.

def EconCSLib.LinearAlgebra.rowEval {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (i : I) (x : Fin n → 𝕜) : 𝕜

Evaluate the LHS of row i of the matrix A : I → Fin n → 𝕜 at the point x : Fin n → 𝕜.

Equations

• EconCSLib.LinearAlgebra.rowEval A i x = ∑ j : Fin n, A i j * x j

def EconCSLib.LinearAlgebra.IsFeasible {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (b : I → 𝕜) : Prop

Primal feasibility of the system A x ≥ b.

Equations

• EconCSLib.LinearAlgebra.IsFeasible A b = ∃ (x : Fin n → 𝕜), ∀ (i : I), b i ≤ EconCSLib.LinearAlgebra.rowEval A i x

def EconCSLib.LinearAlgebra.IsCertificate {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (b u : I → 𝕜) : Prop

u : I → 𝕜 is a Farkas certificate of infeasibility of A x ≥ b.

Equations

• EconCSLib.LinearAlgebra.IsCertificate A b u = ((∀ (i : I), 0 ≤ u i) ∧ (∀ (j : Fin n), ∑ i : I, u i * A i j = 0) ∧ 0 < ∑ i : I, u i * b i)

def EconCSLib.LinearAlgebra.HasCertificate {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (b : I → 𝕜) : Prop

Existence of a Farkas certificate.

Equations

• EconCSLib.LinearAlgebra.HasCertificate A b = ∃ (u : I → 𝕜), EconCSLib.LinearAlgebra.IsCertificate A b u

Disjointness: IsFeasible and HasCertificate cannot both hold

theorem EconCSLib.LinearAlgebra.feas_cert_disjoint {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (b : I → 𝕜) (hfeas : IsFeasible A b) (hcert : HasCertificate A b) : False

Sign partition of rows by the last-column coefficient

For an (n+1)-column matrix A : I → Fin (n+1) → 𝕜 over a Fintype row index I, partition I into the three sign-of-A i (Fin.last n) cases. We use abbrev so Lean's Subtype.fintype instances are transparent.

The generic-I formulation (rather than Fin m) is needed for the induction in theorem_of_alternative_aux: after FM, the row index becomes ZeroRows ⊕ (PosRows × NegRows), which is itself a Fintype but not a Fin _.

@[reducible, inline]

abbrev EconCSLib.LinearAlgebra.ZeroRows {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) : Type u_2

Rows where the last-column coefficient is zero.

Equations

• EconCSLib.LinearAlgebra.ZeroRows A = { i : I // A i (Fin.last n) = 0 }

@[reducible, inline]

abbrev EconCSLib.LinearAlgebra.PosRows {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) : Type u_2

Rows where the last-column coefficient is strictly positive.

Equations

• EconCSLib.LinearAlgebra.PosRows A = { i : I // 0 < A i (Fin.last n) }

@[reducible, inline]

abbrev EconCSLib.LinearAlgebra.NegRows {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) : Type u_2

Rows where the last-column coefficient is strictly negative.

Equations

• EconCSLib.LinearAlgebra.NegRows A = { i : I // A i (Fin.last n) < 0 }

@[reducible, inline]

abbrev EconCSLib.LinearAlgebra.FMRowIndex {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) : Type u_2

Reduced row index after Fourier-Motzkin elimination of the last column.

Equations

• EconCSLib.LinearAlgebra.FMRowIndex A = (EconCSLib.LinearAlgebra.ZeroRows A ⊕ EconCSLib.LinearAlgebra.PosRows A × EconCSLib.LinearAlgebra.NegRows A)

Fourier-Motzkin reduced matrix and RHS

Per blueprint docs/knowledge/nodes/core/linear_algebra.theorem_of_alternative.fourier_motzkin.md:

• zero rows: copy the original row, dropping the last column entry;
• combination rows: for (p, q) ∈ PosRows × NegRows, take the nonneg combination αq · row p + βp · row q with αq = -A q last > 0 and βp = A p last > 0, which annihilates the last column.

def EconCSLib.LinearAlgebra.fmA {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (idx : FMRowIndex A) (j : Fin n) : 𝕜

Reduced matrix coefficient.

Equations

• EconCSLib.LinearAlgebra.fmA A (Sum.inl k) j = A (↑k) j.castSucc
• EconCSLib.LinearAlgebra.fmA A (Sum.inr (p, q)) j = -A (↑q) (Fin.last n) * A (↑p) j.castSucc + A (↑p) (Fin.last n) * A (↑q) j.castSucc

def EconCSLib.LinearAlgebra.fmB {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (idx : FMRowIndex A) : 𝕜

Reduced right-hand side.

Equations

• EconCSLib.LinearAlgebra.fmB A b (Sum.inl k) = b ↑k
• EconCSLib.LinearAlgebra.fmB A b (Sum.inr (p, q)) = -A (↑q) (Fin.last n) * b ↑p + A (↑p) (Fin.last n) * b ↑q

@[simp]

theorem EconCSLib.LinearAlgebra.fmA_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (k : ZeroRows A) (j : Fin n) : fmA A (Sum.inl k) j = A (↑k) j.castSucc

@[simp]

theorem EconCSLib.LinearAlgebra.fmA_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (p : PosRows A) (q : NegRows A) (j : Fin n) : fmA A (Sum.inr (p, q)) j = -A (↑q) (Fin.last n) * A (↑p) j.castSucc + A (↑p) (Fin.last n) * A (↑q) j.castSucc

@[simp]

theorem EconCSLib.LinearAlgebra.fmB_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (k : ZeroRows A) : fmB A b (Sum.inl k) = b ↑k

@[simp]

theorem EconCSLib.LinearAlgebra.fmB_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (p : PosRows A) (q : NegRows A) : fmB A b (Sum.inr (p, q)) = -A (↑q) (Fin.last n) * b ↑p + A (↑p) (Fin.last n) * b ↑q

@[simp]

theorem EconCSLib.LinearAlgebra.rowEval_def {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_3} {n : ℕ} [Fintype I] (A : I → Fin n → 𝕜) (i : I) (x : Fin n → 𝕜) : rowEval A i x = ∑ j : Fin n, A i j * x j

Feasibility transfer (⇒ direction)

If (x_0, ..., x_n) satisfies the original (n+1)-variable system, then (x_0, ..., x_{n-1}) satisfies the reduced n-variable system.

theorem EconCSLib.LinearAlgebra.fm_feasible_of_feasible {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (hfeas : IsFeasible A b) : IsFeasible (fmA A) (fmB A b)

Reduced-pair lower-upper bound

From the reduced inequality at (p, q) ∈ PosRows × NegRows, derive that the lower bound L_p(x') is at most the upper bound U_q(x'). This is the algebraic content of "max lower ≤ min upper" needed to construct x_last.

Feasibility transfer (⇐ direction)

If a solution x' of the reduced system exists, construct an x_last such that Fin.snoc x' x_last solves the original (n+1)-variable system.

theorem EconCSLib.LinearAlgebra.feasible_of_fm_feasible {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (hred : IsFeasible (fmA A) (fmB A b)) : IsFeasible A b

Certificate lift via the transposed FM matrix

The FM reduction can be encoded as a matrix L : FMRowIndex A → Fin m → 𝕜 whose rows are the nonneg coefficients of the original rows feeding into each reduced row. The Farkas certificate of the reduced system lifts to the original via u := L^T u', i.e. u i = ∑ idx, L idx i * u' idx.

def EconCSLib.LinearAlgebra.liftCoeff {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (idx : FMRowIndex A) (i : I) : 𝕜

The FM lift coefficient L idx i: the weight with which original row i enters the reduced row idx.

Equations

• EconCSLib.LinearAlgebra.liftCoeff A (Sum.inl k) i = if ↑k = i then 1 else 0
• EconCSLib.LinearAlgebra.liftCoeff A (Sum.inr (p, q)) i = (if ↑p = i then -A (↑q) (Fin.last n) else 0) + if ↑q = i then A (↑p) (Fin.last n) else 0

theorem EconCSLib.LinearAlgebra.liftCoeff_inl {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (k : ZeroRows A) (i : I) : liftCoeff A (Sum.inl k) i = if ↑k = i then 1 else 0

theorem EconCSLib.LinearAlgebra.liftCoeff_inr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (p : PosRows A) (q : NegRows A) (i : I) : liftCoeff A (Sum.inr (p, q)) i = (if ↑p = i then -A (↑q) (Fin.last n) else 0) + if ↑q = i then A (↑p) (Fin.last n) else 0

def EconCSLib.LinearAlgebra.liftCert {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (u' : FMRowIndex A → 𝕜) (i : I) : 𝕜

The lifted certificate u i = ∑ idx, L idx i * u'(idx).

Equations

• EconCSLib.LinearAlgebra.liftCert A u' i = ∑ idx : EconCSLib.LinearAlgebra.FMRowIndex A, EconCSLib.LinearAlgebra.liftCoeff A idx i * u' idx

theorem EconCSLib.LinearAlgebra.liftCert_nonneg {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) {u' : FMRowIndex A → 𝕜} (hu' : ∀ (idx : FMRowIndex A), 0 ≤ u' idx) (i : I) : 0 ≤ liftCert A u' i

Pointwise nonneg lift.

theorem EconCSLib.LinearAlgebra.fm_cert_lift {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin (n + 1) → 𝕜) (b : I → 𝕜) (hred : HasCertificate (fmA A) (fmB A b)) : HasCertificate A b

Farkas certificate lift: if u' certifies the reduced system, liftCert A u' certifies the original.

Base case n = 0

For a 0-variable system, rowEval A i x = ∑ j : Fin 0, … = 0 for every i, so feasibility collapses to ∀ i, b i ≤ 0. Negation yields a single i with 0 < b i, and the indicator at that i is the Farkas certificate.

Strong induction on the number of columns

Combine: feasibility transfer (feasible_of_fm_feasible) is the contrapositive direction that brings ¬ IsFeasible A b to ¬ IsFeasible (fmA A) (fmB A b); the inductive hypothesis then yields the reduced certificate, and fm_cert_lift lifts it back to the original system.

Final packaged theorem

theorem EconCSLib.LinearAlgebra.theorem_of_alternative {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_3} [Fintype I] [DecidableEq I] {n : ℕ} (A : I → Fin n → 𝕜) (b : I → 𝕜) : ¬IsFeasible A b ↔ HasCertificate A b

Theorem of the Alternative [MFoGT, Section 2.8, Exercise 7]: for a finite system of weak linear inequalities A x ≥ b over a linearly ordered field, exactly one of the primal S = {x | Ax ≥ b} and the Farkas certificate set T = {u ≥ 0 | uᵀA = 0, ⟨u, b⟩ > 0} is nonempty.

Combines feas_cert_disjoint (disjointness) with the existence direction proved by Fourier-Motzkin elimination + induction on the number of variables (theorem_of_alternative_aux).