Cancellation for Fin 4: the structural merge-reduction proof

Every finitely additive epistemic-comparison system on four worlds satisfies Scott cancellation, hence is representable by a finitely additive measure ([HI13] Theorem 8).

Main declarations

• ComparativeProbability.fa_cancellation_fin4 — FA axioms imply cancellation on Fin 4.
• ComparativeProbability.representable_fin4 — every FA system on Fin 4 is representable.
• ComparativeProbability.no_null_cancellation — cancellation for systems with no null atoms.

Implementation notes

The proof rests on two imported layers — conic Carathéodory (Caratheodory.exists_posdep_card_le_five) and the sign-vector core (SignVec.exists_antidom_pair) — and adds the merge reduction: a valid family of comparisons whose vector sum is a single comparison vector proves that comparison (merge_to_single), by a four-rule recursion whose stuck case is discharged through the sign-vector core via v1_tailored. The comparison vector calculus (cmpVec, mergeCmp, cvSumList) and the merge recursion itself are private plumbing; only the theorems above are exported.

Merge-to-single infrastructure

A comparison is a pair of disjoint finsets (pos, neg); its integer vector is 1_pos − 1_neg ∈ {−1,0,1}ⁿ. mergeCmp combines two comparisons whose pos-parts and neg-parts are disjoint into the disjoint-normal-form of their vector sum.

Bridging comparisons to ℚ sign vectors

Denominator-clearing infrastructure

To turn a rational-weighted neutral portfolio into an integer-balanced list of unit comparisons, multiply every weight by the common denominator D and replicate each comparison wc.weight·D times. The helpers below compute the vector sum of such a flatMap-of-replicate list and recover D · weightedSum after casting back to ℚ.

theorem ComparativeProbability.no_null_cancellation (sys : EpistemicSystemFA (Fin 4)) (hnull : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) : Cancellation 4 sys.ge

No-null case of Theorem 8a (Fin 4): when no atom is null, every valid neutral portfolio is non-strict, via the merge reduction merge_to_single.

Fin 3 via lexicographic extension

A Fin 3 system with no null atoms extends to a Fin 4 system by adding a dominant fourth world: comparisons are decided first by membership of the new world, then by the restriction to the original three. The extension preserves the FA axioms and the absence of null atoms, and reflects cancellation, so no_null_cancellation discharges the no-null case of fa_cancellation_fin3; null atoms reduce to representable_fin2. Theorem 8a for Fin 3 then follows from cancellation — replacing the former measure-by-measure case analysis.

def ComparativeProbability.extendFA (sys : EpistemicSystemFA (Fin 3)) : EpistemicSystemFA (Fin 4)

Lexicographic extension: the new world Fin.last 3 dominates; ties break by the restriction.

Equations

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

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

Cancellation for Fin 3, structurally: a null atom reduces to Fin 2 representability; the no-null case extends lexicographically into Fin 4 and pulls back through no_null_cancellation.

theorem ComparativeProbability.representable_fin3 (sys : EpistemicSystemFA (Fin 3)) : Representable sys

Theorem 8a for Fin 3: every FA system on three elements is representable — now derived from Scott cancellation, replacing the former measure-by-measure case analysis.

theorem ComparativeProbability.fa_cancellation_fin4 (sys : EpistemicSystemFA (Fin 4)) : Cancellation 4 sys.ge

Theorem 8a (Fin 4), structural: every FA system on Fin 4 satisfies cancellation. A null atom reduces to Fin 3; the no-null case is the merge reduction no_null_cancellation.

theorem ComparativeProbability.representable_fin4 (sys : EpistemicSystemFA (Fin 4)) : Representable sys

Theorem 8a for Fin 4: every FA system on 4 elements is representable. Via Scott cancellation — see Cancellation.lean for the framework.