Representability of qualitative probability orders

Qualitative probability orders on small domains (|W| ≤ 4) are representable by finitely additive probability measures (Theorem 8a, [kraft-pratt-seidenberg-1959]). For every |W| ≥ 5 this fails: padding the KPS counterexample with null atoms gives a non-representable order at each cardinality (Theorem 8b).

[UPSTREAM] candidate (see the note in Defs.lean).

Contents

1. Representable: the representability predicate.
2. KPS counterexample (Fin 5): non-representable order (kpsSystem, kps_not_representable); null-atom padding (QualitativeProbability.pad, exists_nonrepresentable_fin) extends it to every Fin n with n ≥ 5.
3. Shared infrastructure: null element reduction (null_elem_reduce), representability along equivalences (perm_repr).
4. Small-cardinality proofs: Fin 1 (representable_fin1), Fin 2 (representable_fin2). Fin 3 and Fin 4 are derived from Scott cancellation in CancellationFin4.lean (representable_fin3, representable_fin4).

def ComparativeProbability.Representable {W : Type u_1} (sys : QualitativeProbability (Set W)) : Prop

A qualitative probability order is representable when some finitely additive probability measure induces exactly its comparison relation.

Equations

• ComparativeProbability.Representable sys = ∃ (m : ComparativeProbability.FinAddMeasure ℚ W), ∀ (A B : Set W), sys.le A B ↔ m A ≤ m B

noncomputable def ComparativeProbability.kpsSystem : QualitativeProbability (Set (Fin 5))

Equations

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

theorem ComparativeProbability.kps_not_representable : ¬Representable kpsSystem

theorem ComparativeProbability.reduce_to_disjoint {W : Type u_1} (sys : QualitativeProbability (Set W)) (m : FinAddMeasure ℚ W) (h : ∀ (C D : Set W), Disjoint C D → (sys.le C D ↔ m C ≤ m D)) (A B : Set W) : sys.le A B ↔ m A ≤ m B

Agreement on disjoint pairs suffices for full representability (Axiom A reduces every comparison to a disjoint one).

theorem ComparativeProbability.null_removal_disjoint {W : Type u_1} (sys : QualitativeProbability (Set W)) (j : W) (hj : sys.le {j} ∅) (C D : Set W) (hdisj : Disjoint C D) : sys.le C D ↔ sys.le (C \ {j}) (D \ {j})

Removing a null element (sys.le {j} ∅) from both sides of a disjoint comparison preserves le.

theorem ComparativeProbability.null_elem_reduce {n : ℕ} (sys : QualitativeProbability (Set (Fin (n + 2)))) (hn0 : sys.le {0} ∅) (hnn : ∃ (i : Fin (n + 1)), ¬sys.le {i.succ} ∅) (sub_repr : ∀ (sys' : QualitativeProbability (Set (Fin (n + 1)))), Representable sys') : Representable sys

Null element reduction: if atom 0 is null in an order on Fin (n+2) and some atom is not, representability reduces along Fin.succ to Fin (n+1).

theorem ComparativeProbability.representable_fin1 (sys : QualitativeProbability (Set (Fin 1))) : Representable sys

theorem ComparativeProbability.representable_fin2 (sys : QualitativeProbability (Set (Fin 2))) : Representable sys

theorem ComparativeProbability.transfer_repr {W : Type u_1} {α : Type u_2} (e : W ≃ α) (sys : QualitativeProbability (Set W)) (m : FinAddMeasure ℚ α) (hm : ∀ (A B : Set α), (QualitativeProbability.transport e sys).le A B ↔ m A ≤ m B) (A B : Set W) : sys.le A B ↔ (FinAddMeasure.map (⇑e.symm) m) A ≤ (FinAddMeasure.map (⇑e.symm) m) B

theorem ComparativeProbability.perm_null_iff {n : ℕ} (σ : Fin n ≃ Fin n) (sys : QualitativeProbability (Set (Fin n))) (j : Fin n) : (QualitativeProbability.transport σ sys).le {j} ∅ ↔ sys.le {σ.symm j} ∅

Null pattern transport: j is null in sys.transport σ iff σ.symm j is null in sys.

theorem ComparativeProbability.perm_repr {W : Type u_1} {α : Type u_2} (σ : W ≃ α) (sys : QualitativeProbability (Set W)) (h : Representable (QualitativeProbability.transport σ sys)) : Representable sys

Representability transports backward along any equivalence.

def ComparativeProbability.QualitativeProbability.pad {n : ℕ} (sys : QualitativeProbability (Set (Fin n))) : QualitativeProbability (Set (Fin (n + 1)))

Pad an order with one null atom: comparisons on Fin (n + 1) are decided by the preimage restriction to the first n atoms.

Equations

• sys.pad = { le := fun (A B : Set (Fin (n + 1))) => sys.le (Fin.castSucc ⁻¹' A) (Fin.castSucc ⁻¹' B), mono' := ⋯, nonTrivial := ⋯, total := ⋯, trans' := ⋯, additive := ⋯ }

theorem ComparativeProbability.QualitativeProbability.pad_last_null {n : ℕ} (sys : QualitativeProbability (Set (Fin n))) : sys.pad.le {Fin.last n} ∅

The padded atom is null.

theorem ComparativeProbability.representable_of_pad {n : ℕ} {sys : QualitativeProbability (Set (Fin n))} (h : Representable sys.pad) : Representable sys

Padding reflects representability: a measure for sys.pad assigns the padded atom measure zero, so its Fin.castSucc-image restriction represents sys.

theorem ComparativeProbability.exists_nonrepresentable_fin {n : ℕ} (h : 5 ≤ n) : ∃ (sys : QualitativeProbability (Set (Fin n))), ¬Representable sys

Theorem 8b at every cardinality: for n ≥ 5 there is a non-representable FA system on Fin n — the KPS counterexample, padded with null atoms.