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.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.