Scott cancellation for comparative probability

[KPS59]

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 (Polyhedral.farkas, in Core/Order/FourierMotzkin.lean): 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 declarations

• 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 (in CancellationFin4.lean)
• fa_cancellation_fin4 — FA axioms imply cancellation on Fin 4 (in CancellationFin4.lean)

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

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

Equations

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

structure ComparativeProbability.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 ComparativeProbability.Portfolio (n : ℕ) : Type

A portfolio is a list of weighted comparisons.

Equations

• ComparativeProbability.Portfolio n = List (ComparativeProbability.WComparison n)

def ComparativeProbability.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 : ComparativeProbability.WComparison n) => wc.weight * ↑(ComparativeProbability.comparisonVec n wc.left wc.right i)) P).sum

def ComparativeProbability.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 ComparativeProbability.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 : ComparativeProbability.WComparison n), List.Mem wc P → ge ↑wc.left ↑wc.right

def ComparativeProbability.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 : ComparativeProbability.WComparison n), List.Mem wc P ∧ ¬ge ↑wc.right ↑wc.left

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

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

Equations

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

theorem ComparativeProbability.representable_implies_cancellation {n : ℕ} {ge : Set (Fin n) → Set (Fin n) → Prop} (m : FinAddMeasure ℚ (Fin n)) (hm : ∀ (A B : Set (Fin n)), ge A B ↔ m.inducedGe A B) : Cancellation n 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 ComparativeProbability.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

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

theorem ComparativeProbability.not_all_null {n : ℕ} (sys : EpistemicSystemFA (Fin n)) : ∃ (i : Fin n), ¬sys.ge ∅ {i}

Not all singletons can be null: ∃ i, ¬sys.ge ∅ {i}. If all were null, FA induction gives sys.ge ∅ Set.univ, contradicting nonTrivial.

theorem ComparativeProbability.cancellation_implies_representable {n : ℕ} (sys : EpistemicSystemFA (Fin n)) (hcancel : Cancellation n sys.ge) : Representable sys

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 ComparativeProbability.representable_iff_cancellation {n : ℕ} (sys : EpistemicSystemFA (Fin n)) : Representable sys ↔ Cancellation n sys.ge

Scott's theorem: an FA system is representable by a finitely additive measure iff it satisfies the cancellation property.

theorem ComparativeProbability.cancellation_of_null_atom {n : ℕ} (sys : EpistemicSystemFA (Fin (n + 2))) {j : Fin (n + 2)} (hj : sys.ge ∅ {j}) (sub : ∀ (sys' : EpistemicSystemFA (Fin (n + 1))), Representable sys') : Cancellation (n + 2) sys.ge

A null atom plus a representability oracle one cardinality down yields cancellation: swap the null atom to position 0 and apply null_elem_reduce.