Fin 4 cancellation: dispatch + allpos + main theorem

Auto-generated: dispatches the 88 chamber proofs to prove cancellation for all Fin 4 epistemic systems.

theorem Core.Scale.dispatch_TTT (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_TTF (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_TFT (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_TFF (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_FTT (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_FTF (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_FFT (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.dispatch_FFF (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) (h10 : ¬sys.ge {1} {0}) (h21 : ¬sys.ge {2} {1}) (h32 : ¬sys.ge {3} {2}) : Cancellation 4 sys.ge

theorem Core.Scale.fa_cancellation_fin4_sorted (sys : EpistemicSystemFA (Fin 4)) (hpos : ∀ (i : Fin 4), ¬sys.ge ∅ {i}) (h01 : sys.ge {0} {1}) (h12 : sys.ge {1} {2}) (h23 : sys.ge {2} {3}) : Cancellation 4 sys.ge

Canonical case: 0 ≥ 1 ≥ 2 ≥ 3 with all singletons positive. Dispatches to 88 chambers via 9+ by_cases.

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

theorem Core.Scale.theorem8a_fin4 (sys : EpistemicSystemFA (Fin 4)) : ∃ (m : FinAddMeasure (Fin 4)), ∀ (A B : Set (Fin 4)), sys.ge A B ↔ m.inducedGe A B

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