Fourier-Motzkin elimination and Farkas' lemma over ℚ

Fourier-Motzkin (FM) elimination is a variable-elimination procedure for rational linear inequalities: given a system Ax ≤ b in n+1 variables, eliminate the last variable by combining pairs of constraints (one with positive last coefficient, one with negative) to produce an equisatisfiable system in n variables.

From FM equisatisfiability we derive Farkas' lemma over ℚ: a rational linear system is either feasible or admits a nonneg certificate of infeasibility. This is the core duality theorem for rational linear programming — no topology, no completeness, no ℝ detour. (Mathlib's Farkas, ProperCone.hyperplane_separation, is the topological hyperplane-separation version over ℝ; this constructive ℚ development is complementary.)

Main declarations

• Polyhedral.fmElim — one step of FM elimination (eliminate last variable)
• Polyhedral.fmElim_equisat — FM step preserves feasibility
• Polyhedral.farkas — Farkas' lemma: feasible ∨ infeasibility certificate

Rational linear inequalities

def Polyhedral.dot {n : ℕ} (u v : Fin n → ℚ) : ℚ

Dot product of two rational vectors indexed by Fin n.

Equations

• Polyhedral.dot u v = ∑ i : Fin n, u i * v i

structure Polyhedral.Ineq (n : ℕ) : Type

A linear inequality constraint: lhs · x ≤ rhs.

• lhs : Fin n → ℚ
• rhs : ℚ

def Polyhedral.Ineq.sat {n : ℕ} (c : Ineq n) (x : Fin n → ℚ) : Prop

A constraint is satisfied by a point x when lhs · x ≤ rhs.

Equations

• c.sat x = (Polyhedral.dot c.lhs x ≤ c.rhs)

@[reducible, inline]

abbrev Polyhedral.System (n : ℕ) : Type

A system of linear inequalities (a list of constraints).

Equations

• Polyhedral.System n = List (Polyhedral.Ineq n)

def Polyhedral.System.feasible {n : ℕ} (S : System n) : Prop

A system is feasible if some point satisfies every constraint.

Equations

• S.feasible = ∃ (x : Fin n → ℚ), ∀ c ∈ S, c.sat x

Fourier-Motzkin Elimination Step

def Polyhedral.Ineq.lastCoeff {n : ℕ} (c : Ineq (n + 1)) : ℚ

The last coefficient of a constraint in n+1 variables.

Equations

• c.lastCoeff = c.lhs (Fin.last n)

def Polyhedral.Ineq.project {n : ℕ} (c : Ineq (n + 1)) : Ineq n

Project a constraint to n variables (dropping the last coefficient).

Equations

• c.project = { lhs := fun (i : Fin n) => c.lhs i.castSucc, rhs := c.rhs }

def Polyhedral.Ineq.combine {n : ℕ} (cp cn : Ineq (n + 1)) : Ineq n

Combine a positive-last and negative-last constraint, eliminating the last variable.

Equations

• cp.combine cn = { lhs := fun (i : Fin n) => -cn.lastCoeff * cp.lhs i.castSucc + cp.lastCoeff * cn.lhs i.castSucc, rhs := -cn.lastCoeff * cp.rhs + cp.lastCoeff * cn.rhs }

def Polyhedral.fmElim {n : ℕ} (S : System (n + 1)) : System n

One step of FM elimination: partition constraints by sign of the last coefficient, project the zero ones, combine all positive × negative pairs.

Equations

• One or more equations did not get rendered due to their size.

FM Equisatisfiability

theorem Polyhedral.fmElim_equisat {n : ℕ} (S : System (n + 1)) : S.feasible ↔ (fmElim S).feasible

FM equisatisfiability: the original system (n+1 variables) is feasible iff the reduced system (n variables) is feasible.

Forward: project out last coordinate. Backward: find t in the interval defined by positive (upper bound) and negative (lower bound) constraints; the P×N combinations guarantee the interval is nonempty.

Farkas' Lemma

structure Polyhedral.InfeasCert {n : ℕ} (S : System n) : Type

An infeasibility certificate: nonneg weights (indexed by constraint position) such that the weighted combination of constraints yields 0·x ≤ negative.

• ws : Fin (List.length S) → ℚ
• nonneg (i : Fin (List.length S)) : 0 ≤ self.ws i
• coeffsZero (j : Fin n) : ∑ i : Fin (List.length S), self.ws i * (List.get S i).lhs j = 0
• boundNeg : ∑ i : Fin (List.length S), self.ws i * (List.get S i).rhs < 0

theorem Polyhedral.farkas {n : ℕ} (S : System n) : S.feasible ∨ Nonempty (InfeasCert S)

Farkas' lemma over ℚ: a rational linear system is either feasible or has a nonneg certificate of infeasibility.

Proof by induction on n (number of variables), using FM elimination. Base case (0 variables): each constraint is 0 ≤ rhs. Inductive step: FM-eliminate → IH → extend backward or lift certificate.