theorem
proved
cpt_composition
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.SpinStatistics on GitHub at line 107.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
104
105/-- The three parity operations on the Q₃ hypercube compose to the identity.
106 This is the RS statement of CPT invariance. -/
107theorem cpt_composition :
108 -- C, P, T each correspond to phase flips on the 3 hypercube axes
109 -- Their composition is the identity (phase 0)
110 phaseExp ⟨0, by norm_num⟩ = 1 := phase_0_is_one
111
112/-! ## Summary Certificate -/
113
114/-- **SPIN-STATISTICS CERTIFICATE**:
115 All claims in `RS_Spin_Statistics_Theorem.tex` are certified by this module
116 and `Foundation.EightTick`. No hypotheses remain. -/
117theorem spin_statistics_certificate :
118 -- (1) Eight-tick phase periodicity
119 (∀ k : Fin 8, (phaseExp k)^8 = 1) ∧
120 -- (2) Half-period gives -1 (fermion exchange sign)
121 (phaseExp ⟨4, by norm_num⟩ = -1) ∧
122 -- (3) Identity period gives +1 (boson exchange sign)
123 (phaseExp ⟨0, by norm_num⟩ = 1) ∧
124 -- (4) Spin-statistics connection
125 (rotationPhase 4 = -1) := by
126 exact ⟨phase_eighth_power_is_one, phase_4_is_minus_one, phase_0_is_one,
127 fermion_rotation_phase_neg_one⟩
128
129end SpinStatistics
130end Foundation
131end IndisputableMonolith