no_sm_falsifier
plain-language theorem explainer
The declaration confirms that exchange symmetry derived from spin matches the fermion-boson distinction for the five lowest spin values realized in nature. A physicist examining discrete-time derivations of the spin-statistics theorem would cite it to verify that the eight-tick phase rule reproduces Standard Model assignments without contradiction. The proof is a one-line term-mode wrapper that reduces to reflexivity after introducing the spin value.
Claim. For every spin quantum number $p$ in the set containing spin zero, half, one, three-halves and two, the exchange symmetry of the two-particle wave function equals the antisymmetric type precisely when $p$ is half-integer and the symmetric type otherwise.
background
Spin is the structure whose field twice : ℤ records twice the usual spin value, with the nonnegativity guard ensuring non-negative half-integers. ExchangeSymmetry is the inductive type with constructors symmetric and antisymmetric that classifies wave-function behavior under particle interchange. The module setting is the eight-tick cycle in which a 2π rotation traverses eight fundamental ticks; half-integer spins require two full cycles and therefore accumulate a phase factor of -1. Upstream, the phase function from EightTick supplies the explicit kπ/4 values for k = 0..7, while the tick constant fixes the discrete time quantum.
proof idea
The proof is a one-line term-mode wrapper. After the intro p _ tactic discards the membership hypothesis, reflexivity closes the goal because exchangeSymmetryFromSpin is definitionally equal to the conditional expression on isHalfInteger.
why it matters
The result anchors the spin-statistics connection by showing that the eight-tick phase rule assigns antisymmetric statistics exactly to the half-integer spins that appear in the Standard Model. It directly supports the QFT-002 claim that fermions accumulate an odd phase through the cycle. The declaration sits downstream of EightTick.phase and the Spin structure; with used_by_count zero it functions as a base consistency check rather than feeding a larger parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.