SpinStatisticsFalsifier
plain-language theorem explainer
SpinStatisticsFalsifier assembles a spin quantum number, an observed exchange symmetry, and an explicit mismatch witness against the map that assigns symmetry from the eight-tick phase rule. A physicist auditing the Recognition Science derivation of spin-statistics would cite this record when constructing or searching for counterexamples. The definition is a plain three-field structure with no computation or lemmas.
Claim. A falsifier consists of a spin quantum number $s$, an observed exchange symmetry type $σ$ (symmetric or antisymmetric), and a witness that the symmetry predicted by the eight-tick phase rule from $s$ differs from $σ$.
background
Spin is the structure holding twice the spin value as an integer together with a non-negativity proof; it encodes half-integer or integer values. ExchangeSymmetry is the inductive type with constructors symmetric and antisymmetric that records the sign of the wavefunction under particle exchange. The module derives the spin-statistics link from Recognition Science's eight-tick octave: a $2π$ rotation traverses eight ticks, half-integer spins require two full cycles and accumulate phase $-1$, while integer spins accumulate phase $+1$ (see MODULE_DOC). Upstream, exchangeSymmetryFromSpin directly implements the map that returns antisymmetric for half-integer spin and symmetric otherwise.
proof idea
The declaration is a plain record type whose fields are spin, observed, and the inequality exchangeSymmetryFromSpin spin ≠ observed. No tactics, lemmas, or reductions are applied; the structure simply packages the three components of a potential counterexample.
why it matters
This record supplies the formal shape of any counterexample to the spin-statistics theorem obtained from the eight-tick phase accumulation. It stands ready for use in searches for violations of the derived fermion-boson distinction. The parent derivation is the module's core claim that phase accumulation through the eight-tick cycle (T7) reproduces the standard relation between spin and exchange symmetry. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.