`spin_statistics_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SpinStatistics
domain: Foundation
line: 117 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SpinStatistics on GitHub at line 117.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.