statisticsFromSpin
plain-language theorem explainer
The definition maps a spin quantum number to Fermi-Dirac statistics when the spin is half-integer and to Bose-Einstein statistics otherwise. Researchers deriving the spin-statistics theorem from discrete 8-tick phase cycles cite it as the direct link between spin parity and thermodynamic distributions. It is implemented as a single conditional on the parity of twice the spin value.
Claim. For a spin quantum number $s$, the statistics type equals Fermi-Dirac if $s$ is half-integer and Bose-Einstein otherwise.
background
Spin is the structure holding twice the spin value as a non-negative integer. Statistics is the inductive type with constructors fermiDirac and boseEinstein. The module derives the spin-statistics connection from Recognition Science's 8-tick phase cycle, where a $2π$ rotation traverses one full cycle and half-integer spins require two cycles to return to identity. Upstream, isHalfInteger checks whether twice the spin value is odd.
proof idea
The definition is a one-line conditional that returns Statistics.fermiDirac precisely when isHalfInteger holds and Statistics.boseEinstein otherwise.
why it matters
This definition supplies the mapping used by the spin_statistics_fermion and spin_statistics_boson theorems, which establish the full spin-statistics link. It realizes the module's core claim that phase accumulation through the eight-tick octave forces antisymmetric statistics for half-integer spins. The result sits inside the QFT-001 derivation of spin-statistics from discrete time structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.