spin_statistics_theorem
plain-language theorem explainer
The Recognition Science spin-statistics theorem equates the exchange sign of two-particle states to the phase each particle acquires under 2π rotation in the discrete eight-tick group. Researchers deriving quantum statistics from a single functional equation and discrete symmetries would cite this result. The proof is a one-line wrapper that invokes the spin_statistics_key lemma from the EightTick module.
Claim. In the Recognition Science eight-tick ledger, the rotation phase for a 4-tick fermion satisfies rotationPhase(4) = -1, forcing antisymmetry under exchange, while the phase for the 0-tick boson identity satisfies phaseExp(0) = 1, forcing symmetry under exchange.
background
The module derives the spin-statistics connection from the RS eight-tick structure, where phases live in the cyclic group ℤ/8ℤ. The function phaseExp(k) for k : Fin 8 is the complex exponential exp(i · phase(k)). The upstream spin_statistics_key theorem states that phaseExp(4) = -1 and phaseExp(0) = 1, linking the discrete symmetry group directly to fermion and boson exchange signs. This rests on the eight-tick octave, which generates the discrete symmetry group of RS.
proof idea
The proof is a one-line wrapper that applies the spin_statistics_key theorem from Foundation.EightTick. That lemma supplies the two phase equalities phaseExp ⟨4⟩ = -1 and phaseExp ⟨0⟩ = 1, with the rotationPhase(4) = -1 identification already established in the module.
why it matters
This theorem realizes the eight-tick octave (T7) by showing how discrete rotation phases enforce the exchange symmetries of fermions and bosons. It completes the spin-statistics derivation in the Recognition Science framework and supplies the certificate referenced in RS_Spin_Statistics_Theorem.tex. The result closes the step from the eight-tick ledger to the standard quantum statistics without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.