Fourier-Motzkin Elimination, Farkas' Lemma, and Cancellation

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.

Cancellation conditions for comparative probability

@cite{kraft-pratt-seidenberg-1959}

Scott's cancellation framework for representability of comparative probability orderings by finitely additive measures. A comparative probability ordering ≿ is representable by a finitely additive measure iff it satisfies the cancellation property: no valid neutral portfolio has a strict member.

The hard direction (cancellation → representable) is an instance of LP duality / Farkas' lemma: the feasibility polytope {p ≥ 0 : Σpᵢ = 1, ordering constraints} is nonempty iff no dual certificate of infeasibility exists, and such a certificate corresponds exactly to a neutral portfolio with a strict member.

Main results

• Polyhedral.fmElim — one step of FM elimination (eliminate last variable)
• Polyhedral.fmElim_equisat — FM step preserves feasibility
• Polyhedral.farkas — Farkas' lemma: feasible ∨ infeasibility certificate
• representable_implies_cancellation — easy direction: measure existence → cancellation
• cancellation_implies_representable — hard direction: cancellation → measure existence (via feasibleWeights, cancellation_nonempty, feasible_to_measure)
• fa_cancellation_fin3 — FA axioms imply cancellation on Fin 3
• fa_cancellation_fin4 — FA axioms imply cancellation on Fin 4 (in Cancellation88.lean)
• theorem8a_fin3' — KPS Theorem 8a for n = 3 (via cancellation)

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

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.

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.

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.

def Core.Scale.comparisonVec (n : ℕ) (A B : Finset (Fin n)) : Fin n → ℤ

Characteristic vector of a disjoint comparison: χ_A - χ_B ∈ {-1,0,1}ⁿ

Equations

• Core.Scale.comparisonVec n A B i = (if i ∈ A then 1 else 0) - if i ∈ B then 1 else 0

structure Core.Scale.WComparison (n : ℕ) : Type

A weighted comparison: a disjoint pair (A,B) with positive rational weight.

• left : Finset (Fin n)
• right : Finset (Fin n)
• weight : ℚ
• disjoint : Disjoint self.left self.right
• weight_pos : 0 < self.weight

def Core.Scale.Portfolio (n : ℕ) : Type

A portfolio is a list of weighted comparisons.

Equations

• Core.Scale.Portfolio n = List (Core.Scale.WComparison n)

def Core.Scale.Portfolio.weightedSum {n : ℕ} (P : Portfolio n) (i : Fin n) : ℚ

The weighted sum of comparison vectors at atom i.

Equations

• P.weightedSum i = (List.map (fun (wc : Core.Scale.WComparison n) => wc.weight * ↑(Core.Scale.comparisonVec n wc.left wc.right i)) P).sum

def Core.Scale.Portfolio.isNeutral {n : ℕ} (P : Portfolio n) : Prop

A portfolio is neutral if weighted vectors sum to zero at every atom.

Equations

• P.isNeutral = ∀ (i : Fin n), P.weightedSum i = 0

def Core.Scale.Portfolio.isValid {n : ℕ} (P : Portfolio n) (ge : Set (Fin n) → Set (Fin n) → Prop) : Prop

A portfolio is valid for an ordering if each comparison holds.

Equations

• P.isValid ge = ∀ (wc : Core.Scale.WComparison n), List.Mem wc P → ge ↑wc.left ↑wc.right

def Core.Scale.Portfolio.hasStrict {n : ℕ} (P : Portfolio n) (ge : Set (Fin n) → Set (Fin n) → Prop) : Prop

A portfolio has a strict member if at least one comparison is strict.

Equations

• P.hasStrict ge = ∃ (wc : Core.Scale.WComparison n), List.Mem wc P ∧ ¬ge ↑wc.right ↑wc.left

def Core.Scale.Cancellation (n : ℕ) (ge : Set (Fin n) → Set (Fin n) → Prop) : Prop

The cancellation property: no valid neutral portfolio has a strict member.

Equations

• Core.Scale.Cancellation n ge = ∀ (P : Core.Scale.Portfolio n), P.isValid ge → P.isNeutral → ¬P.hasStrict ge

theorem Core.Scale.representable_implies_cancellation {n : ℕ} (sys : EpistemicSystemFA (Fin n)) (m : FinAddMeasure (Fin n)) (hm : ∀ (A B : Set (Fin n)), sys.ge A B ↔ m.inducedGe A B) : Cancellation n sys.ge

Easy direction: If μ represents the ordering, no neutral portfolio has a strict member. Each comparison contributes wⱼ·(μ(Aⱼ)−μ(Bⱼ)) ≥ 0 to the portfolio value; if any is strict, the value is positive. But by the interchange lemma, the value also equals Σᵢ μ({i})·weightedSum(i) = 0 by neutrality.

def Core.Scale.feasibleWeights (n : ℕ) (sys : EpistemicSystemFA (Fin n)) : Set (Fin n → ℚ)

The feasibility polytope for measure representation: probability vectors p : Fin n → ℚ that are nonneg, normalized, and faithfully encode the ordering on disjoint pairs — exactly sys.ge ↑A ↑B ↔ A.sum p ≥ B.sum p. The ↔ (rather than →) is essential: the forward direction ensures the measure respects the ordering, while the backward direction ensures strictness is preserved (no spurious ties).

Equations

• Core.Scale.feasibleWeights n sys = {p : Fin n → ℚ | (∀ (i : Fin n), 0 ≤ p i) ∧ Finset.univ.sum p = 1 ∧ ∀ (A B : Finset (Fin n)), Disjoint A B → (sys.ge ↑A ↑B ↔ A.sum p ≥ B.sum p)}

theorem Core.Scale.cancellation_implies_representable {n : ℕ} (sys : EpistemicSystemFA (Fin n)) (hcancel : Cancellation n sys.ge) : ∃ (m : FinAddMeasure (Fin n)), ∀ (A B : Set (Fin n)), sys.ge A B ↔ m.inducedGe A B

Scott's theorem (hard direction): if no valid neutral portfolio has a strict member, then a finitely additive measure exists representing the ordering. Decomposes into two steps:

1. cancellation_nonempty: Farkas / LP duality shows the feasibility polytope is nonempty when cancellation holds.
2. feasible_to_measure: a feasible weight vector constructs a representing FinAddMeasure.

theorem Core.Scale.fa_cancellation_fin3 (sys : EpistemicSystemFA (Fin 3)) : Cancellation 3 sys.ge

FA on Fin 3 implies the cancellation property. Derived from the direct measure construction (theorem8a_fin3 in Defs.lean) composed with the easy direction of Scott's theorem.

theorem Core.Scale.not_all_null_fin4 (sys : EpistemicSystemFA (Fin 4)) (h0 : sys.ge ∅ {0}) (h1 : sys.ge ∅ {1}) (h2 : sys.ge ∅ {2}) (h3 : sys.ge ∅ {3}) : False

Not all 4 singletons can be null (non-triviality).

theorem Core.Scale.fa_cancellation_fin4_null0 (sys : EpistemicSystemFA (Fin 4)) (h0 : sys.ge ∅ {0}) (hnn : ∃ (i : Fin 3), ¬sys.ge ∅ {i.succ}) : Cancellation 4 sys.ge

Helper: if element 0 is null on Fin 4, derive cancellation via null reduction to Fin 3.

theorem Core.Scale.cancellation_from_weights {n : ℕ} (sys : EpistemicSystemFA (Fin n)) (p : Fin n → ℚ) (hp : ∀ (i : Fin n), 0 < p i) (hsum : Finset.univ.sum p = 1) (hfwd : ∀ (A B : Finset (Fin n)), Disjoint A B → sys.ge ↑A ↑B → A.sum p ≥ B.sum p) (hstrict : ∀ (A B : Finset (Fin n)), Disjoint A B → sys.ge ↑A ↑B → ¬sys.ge ↑B ↑A → A.sum p > B.sum p) : Cancellation n sys.ge

Cancellation follows from a "forward + strict" witness: positive weights p summing to 1 such that every valid comparison has p-value ≥ 0 and every strict comparison has p-value > 0. This avoids constructing a full representing measure.

theorem Core.Scale.cancellation_from_weights_fin4 (sys : EpistemicSystemFA (Fin 4)) (p : Fin 4 → ℚ) (hp : ∀ (i : Fin 4), 0 < p i) (hsum : Finset.univ.sum p = 1) (hnge : ∀ (A B : Finset (Fin 4)), Disjoint A B → A.sum p < B.sum p → ¬sys.ge ↑A ↑B) (heq : ∀ (A B : Finset (Fin 4)), Disjoint A B → A.sum p = B.sum p → sys.ge ↑A ↑B → sys.ge ↑B ↑A) : Cancellation 4 sys.ge

Wrapper around cancellation_from_weights that replaces the two universally-quantified obligations (hfwd, hstrict) with a single contrapositive condition: for every disjoint pair (A, B) where A.sum p < B.sum p, we have ¬sys.ge ↑A ↑B. Equal-sum pairs need bidirectionality (heq). The proof of cancellation_from_weights does the hfwd/hstrict dispatch once; each chamber only provides the ~5-10 ¬ge facts for "wrong-direction" pairs.

theorem Core.Scale.ge_empty_contra (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) {B : Set (Fin 4)} (hne : B.Nonempty) (h : sys.ge ∅ B) : False

ge(∅, B) is impossible when B is nonempty and ¬ge(∅, {i}) for all singletons.

theorem Core.Scale.cancellation_from_pairs (sys : EpistemicSystemFA (Fin 4)) (p : Fin 4 → ℚ) (hp : ∀ (i : Fin 4), 0 < p i) (hsum : Finset.univ.sum p = 1) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (lt_pairs : List (Finset (Fin 4) × Finset (Fin 4))) (hlt_cover : ∀ (A B : Finset (Fin 4)), A.Nonempty → B.Nonempty → Disjoint A B → A.sum p < B.sum p → (A, B) ∈ lt_pairs) (hlt : ∀ pair ∈ lt_pairs, ¬sys.ge ↑pair.1 ↑pair.2) (eq_pairs : List (Finset (Fin 4) × Finset (Fin 4))) (heq_cover : ∀ (A B : Finset (Fin 4)), A.Nonempty → B.Nonempty → Disjoint A B → A.sum p = B.sum p → (A, B) ∈ eq_pairs) (heq : ∀ pair ∈ eq_pairs, sys.ge ↑pair.1 ↑pair.2 → sys.ge ↑pair.2 ↑pair.1) : Cancellation 4 sys.ge

Pre-computed pair variant of cancellation_from_weights_fin4. Instead of 256-case dispatch via finset_fin4_eq, the caller provides explicit lists of critical (A,B) pairs and proves coverage via native_decide. Empty-set cases are handled internally via ge_empty_contra.

theorem Core.Scale.cancellation_from_generic_weights {n : ℕ} (sys : EpistemicSystemFA (Fin n)) (p : Fin n → ℚ) (hp : ∀ (i : Fin n), 0 < p i) (hsum : Finset.univ.sum p = 1) (hfwd : ∀ (A B : Finset (Fin n)), Disjoint A B → sys.ge ↑A ↑B → A.sum p ≥ B.sum p) (hgeneric : ∀ (A B : Finset (Fin n)), Disjoint A B → A.sum p = B.sum p → A = ∅ ∧ B = ∅) : Cancellation n sys.ge

When weights are generic (no two nonempty disjoint subsets have equal sum), cancellation reduces to a single forward obligation: sys.ge ↑A ↑B → A.sum p ≥ B.sum p. The strict direction and equal-sum bidirectionality are both free:

• strict: contrapositive of hfwd (if A.sum p < B.sum p then ¬sys.ge ↑A ↑B)
• heq: vacuously true (genericity rules out equal-sum disjoint pairs)

theorem Core.Scale.finset_fin4_eq (S : Finset (Fin 4)) : S = ∅ ∨ S = {0} ∨ S = {1} ∨ S = {2} ∨ S = {3} ∨ S = {0, 1} ∨ S = {0, 2} ∨ S = {0, 3} ∨ S = {1, 2} ∨ S = {1, 3} ∨ S = {2, 3} ∨ S = {0, 1, 2} ∨ S = {0, 1, 3} ∨ S = {0, 2, 3} ∨ S = {1, 2, 3} ∨ S = Finset.univ

Classify all Finset (Fin 4) into one of 16 explicit values.

theorem Core.Scale.nge_13_02 (sys : EpistemicSystemFA (Fin 4)) (h01 : sys.ge {0} {1}) (h23 : sys.ge {2} {3}) (h : ¬sys.ge {1} {0} ∨ ¬sys.ge {3} {2}) : ¬sys.ge {1, 3} {0, 2}

¬ge({1,3}, {0,2}) from singleton hypotheses via additive decomposition. Route A (¬ge({1},{0})): ge({1,3},{0,2}) → additive ge({0,2},{0,3}) via ge({2},{3}) → trans → ge({1,3},{0,3}) → additive → ge({1},{0}) → contradiction. Route B (¬ge({3},{2})): ge({1,3},{0,2}) → additive ge({0,2},{1,2}) via ge({0},{1}) → trans → ge({1,3},{1,2}) → additive → ge({3},{2}) → contradiction.

theorem Core.Scale.nge_23_01 (sys : EpistemicSystemFA (Fin 4)) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h01 : sys.ge {0} {1}) (h : ¬sys.ge {2} {0} ∨ ¬sys.ge {3} {1}) : ¬sys.ge {2, 3} {0, 1}

¬ge({2,3}, {0,1}) from singleton hypotheses via additive decomposition. Route A (¬ge({2},{0})): ge({2,3},{0,1}) → additive ge({0,1},{0,3}) via ge({1},{3}) → trans → ge({2,3},{0,3}) → additive → ge({2},{0}) → contradiction. Route B (¬ge({3},{1})): ge({2,3},{0,1}) → additive ge({0,1},{1,2}) via ge({0},{2}) → trans → ge({2,3},{1,2}) → additive → ge({3},{1}) → contradiction.

theorem Core.Scale.perm_cancellation {n : ℕ} (σ : Fin n ≃ Fin n) (sys : EpistemicSystemFA (Fin n)) (hc : Cancellation n (transportFA σ sys).ge) : Cancellation n sys.ge

Cancellation transfers through permutations (via representability).

theorem Core.Scale.theorem8a_fin3' (sys : EpistemicSystemFA (Fin 3)) : ∃ (m : FinAddMeasure (Fin 3)), ∀ (A B : Set (Fin 3)), sys.ge A B ↔ m.inducedGe A B

Theorem 8a for Fin 3 (via cancellation): every FA system on Fin 3 is representable by a finitely additive probability measure.