spin_statistics_boson
plain-language theorem explainer
Integer spin particles obey Bose-Einstein statistics in the Recognition Science 8-tick framework. Physicists deriving QFT phase rules from discrete time would cite this result. The proof unfolds the statistics assignment and reaches a contradiction by combining the integer hypothesis with the half-integer assumption via mutual exclusivity.
Claim. If the spin quantum number $s$ satisfies the integer condition (twice the spin value is even), then the associated statistics type is Bose-Einstein.
background
Spin is the structure holding twice the spin value as a non-negative integer. The integer predicate holds precisely when this value is even. Statistics is the inductive type with constructors Fermi-Dirac and Bose-Einstein; the assignment function returns Bose-Einstein exactly when the spin is integer and Fermi-Dirac when half-integer.
proof idea
The term proof first simplifies the statistics assignment definition. It then introduces the half-integer assumption and applies the mutual-exclusivity lemma to the pair of integer and half-integer hypotheses, yielding an absurdity.
why it matters
The result supplies one half of the spin-statistics link inside the QFT module that extracts the connection from the 8-tick cycle. It feeds the downstream eight-ticks-full-cycle theorem that computes the accumulated phase after eight ticks. The derivation realizes the module's core claim that integer spins produce phase factor +1 after one cycle while half-integer spins produce -1 after two cycles, aligning with the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.