KPS representation and completeness theorems

The top-level representation results ([kraft-pratt-seidenberg-1959]; [van-der-hoek-1996]):

• ComparativeProbability.representable_of_card_lt_five — for |W| < 5, every FA model is representable by a finitely additive probability measure (FA = FP∞ below five worlds).
• ComparativeProbability.exists_nonrepresentable_of_five_le_card — for |W| ≥ 5, FA is strictly weaker than FP∞ (the KPS counterexample, padded with null atoms).
• ComparativeProbability.exists_qualAddMeasure_repr — every order on a finite carrier is represented by a qualitatively additive measure ([van-der-hoek-1996]).
• ComparativeProbability.axiomA_iff_fa — Axiom A is equivalent to disjoint-union invariance (finite additivity).

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

theorem ComparativeProbability.representable_of_card_lt_five {W : Type u_1} [Fintype W] (sys : QualitativeProbability (Set W)) (hcard : Fintype.card W < 5) : Representable sys

Kraft–Pratt–Seidenberg, below five atoms ([kraft-pratt-seidenberg-1959]): every qualitative probability order on fewer than five atoms is representable by a finitely additive measure.

theorem ComparativeProbability.exists_nonrepresentable_of_five_le_card {W : Type u_1} [Fintype W] (hcard : 5 ≤ Fintype.card W) : ∃ (sys : QualitativeProbability (Set W)), ¬Representable sys

Kraft–Pratt–Seidenberg, at five or more atoms ([kraft-pratt-seidenberg-1959]): some qualitative probability order is not representable by any finitely additive measure.

theorem ComparativeProbability.exists_qualAddMeasure_repr {W : Type u_1} [Fintype W] (sys : QualitativeProbability (Set W)) : ∃ (m : QualAddMeasure ℚ W), ∀ (A B : Set W), sys.le A B ↔ m A ≤ m B

Qualitatively additive representation ([van-der-hoek-1996]): every qualitative probability order on a finite carrier is representable by a qualitatively additive measure — the dominated-set count, affinely renormalised so μ(∅) = 0 and μ(Ω) = 1.

theorem ComparativeProbability.axiomA_iff_fa {W : Type u_1} (ge : Set W → Set W → Prop) : (∀ (A B : Set W), ge A B ↔ ge (A \ B) (B \ A)) ↔ ∀ (A B C : Set W), (∀ x ∈ A, x ∉ C) → (∀ x ∈ B, x ∉ C) → (ge A B ↔ ge (A ∪ C) (B ∪ C))

Algebraic bridge: Axiom A and finite additivity (disjoint augmentation preserves the comparison) are equivalent for any comparison on sets.