spin_statistics_fermion
plain-language theorem explainer
Half-integer spin particles obey Fermi-Dirac statistics in the Recognition Science derivation of the spin-statistics theorem. A physicist working on discrete-time origins of QFT would cite this when linking spin to exchange symmetry via phase accumulation. The proof is a one-line simplification that unfolds the statistics assignment and matches the given half-integer hypothesis.
Claim. Let $s$ be a spin quantum number. If twice the value of $s$ is odd, then the statistics assigned to $s$ is Fermi-Dirac.
background
Spin is the structure whose field twice : ℤ records twice the spin value (ensuring integer arithmetic) together with a non-negativity guard. The predicate isHalfInteger holds exactly when twice modulo 2 equals 1, marking fermions. Statistics is the inductive type with constructors fermiDirac and boseEinstein; the function statisticsFromSpin returns fermiDirac precisely on the isHalfInteger branch.
proof idea
The proof is a one-line wrapper that applies simp to unfold statisticsFromSpin and discharge the goal with the supplied hypothesis that s.isHalfInteger.
why it matters
This theorem supplies the fermion half of the spin-statistics connection inside the QFT module and is invoked by the eight-ticks-full-cycle result. It realizes the module's core claim that half-integer spins accumulate a phase factor of -1 after one 8-tick cycle, producing antisymmetric wavefunctions. The result sits at the T7 eight-tick octave step of the forcing chain and supplies the discrete-time origin of the conventional spin-statistics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.