Statistics
plain-language theorem explainer
The Statistics inductive type enumerates the two exchange symmetries for particles in Recognition Science QFT. Researchers deriving spin-statistics from the eight-tick phase cycle cite it to separate half-integer spin fermions from integer spin bosons. The definition is a direct inductive enumeration deriving decidable equality and representation.
Claim. Particle statistics form an inductive type with two cases: Fermi-Dirac (antisymmetric under exchange) and Bose-Einstein (symmetric under exchange).
background
The QFT module derives the spin-statistics theorem from Recognition Science's eight-tick phase structure. A full 2π rotation traverses one 8-tick cycle; half-integer spins accumulate phase -1 after two cycles while integer spins accumulate +1 after one cycle. This yields the standard distinction between fermions and bosons via phase parity.
proof idea
This is an inductive definition introducing two constructors for the statistics types together with derived decidable equality and representation instances. No lemmas or tactics are applied.
why it matters
The definition supplies the type used by downstream results including boson_symmetric, exchange_sign_boson, and the QFT summary. It directly implements the QFT-001 target of obtaining spin-statistics from the eight-tick cycle, linking to the T7 eight-tick octave and the phase mechanism in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.