Cancellation on at most four atoms

Every qualitative probability order on at most four atoms satisfies Scott cancellation, hence is representable by a probability measure, as Kraft, Pratt and Seidenberg showed.

Main declarations

• ComparativeProbability.no_null_cancellation: cancellation on Fin 4 with no null atoms.
• ComparativeProbability.extendLex: the extension by a dominant world.
• ComparativeProbability.cancellation_of_le_four: every qualitative probability on at most four atoms satisfies cancellation.
• ComparativeProbability.representable_of_le_four: every qualitative probability on at most four atoms is representable.

Implementation notes

On Fin 4 with no null atom the proof is the merge reduction: a valid family of comparisons whose integer sum is a single sign vector proves that comparison (merge_to_single), by a four-rule recursion whose stuck case is discharged through the sign-vector core (Balanced.exists_antiDominating) via v1_tailored. Comparisons are Scott.lean's sign vectors; two comparisons with no shared nonzero coordinate merge into the sign of their sum (merge). Smaller sizes reach this case by the lexicographic extension, and a null atom drops to one atom fewer, so a single induction covers every size up to four.

References

• [KPS59]

Merging comparisons

Two sign vectors are mergeable when no coordinate carries the same nonzero sign in both; their merge is the sign of their sum, which is then their sum.

The stuck case of the merge recursion

theorem ComparativeProbability.no_null_cancellation (r : Set (Fin 4) → Set (Fin 4) → Prop) [IsQualitativeProbability r] (hnull : ∀ (i : Fin 4), ¬r ∅ {i}) : Cancellation r

A qualitative probability on Fin 4 with no null atom satisfies cancellation, by the merge reduction merge_to_single.

Fewer atoms by lexicographic extension

A qualitative probability on Fin n with no null atom extends to Fin (n + 1) by adding a dominant world: comparisons are decided first by membership of the new world, then by the restriction to the original ones. The extension preserves the axioms and the absence of null atoms, and reflects cancellation, so iterating it carries the no-null case of every size up to four to no_null_cancellation; a null atom reduces to one atom fewer.

def ComparativeProbability.extendLex {n : ℕ} (r : Set (Fin n) → Set (Fin n) → Prop) (A B : Set (Fin (n + 1))) : Prop

extendLex r extends a relation on Fin n to Fin (n + 1) by a new world Fin.last n that dominates: an event holding at the new world is more likely than one that does not, and ties are broken by the restriction along Fin.castSucc.

Equations

• ComparativeProbability.extendLex r A B = (Fin.last n ∈ A ∧ Fin.last n ∉ B ∨ (Fin.last n ∈ A ↔ Fin.last n ∈ B) ∧ r (Fin.castSucc ⁻¹' A) (Fin.castSucc ⁻¹' B))

instance ComparativeProbability.instIsQualitativeProbabilitySetFinHAddNatOfNatExtendLex {n : ℕ} {r : Set (Fin n) → Set (Fin n) → Prop} [IsQualitativeProbability r] : IsQualitativeProbability (extendLex r)

theorem ComparativeProbability.cancellation_of_le_four {n : ℕ} : n ≤ 4 → ∀ (r : Set (Fin n) → Set (Fin n) → Prop) [IsQualitativeProbability r], Cancellation r

Every qualitative probability on at most four atoms satisfies cancellation. A null atom reduces to one atom fewer (cancellation_of_null_atom); otherwise the lexicographic extension to Fin 4 applies.

theorem ComparativeProbability.representable_of_le_four {n : ℕ} (hn : n ≤ 4) (r : Set (Fin n) → Set (Fin n) → Prop) [IsQualitativeProbability r] : Representable r

Every qualitative probability on at most four atoms is representable, by Scott cancellation.