Spin
plain-language theorem explainer
The structure for spin quantum numbers encodes the value as a non-negative half-integer by storing twice the spin as an integer. Physicists deriving the spin-statistics connection from eight-tick phase cycles would cite this when characterizing spinors in three dimensions. It is defined directly as a structure with an integer field and a nonnegativity condition.
Claim. A spin quantum number $s$ is represented by an integer $n=2s$ with $n$ nonnegative, so that the physical value is $s=n/2$.
background
The QFT-001 module derives the spin-statistics theorem from the eight-tick phase structure. A 2π rotation traverses one full cycle, producing phase factor exp(2π i s). When the integer n is odd the factor equals -1 (fermion); when even it equals +1 (boson). Antisymmetry under exchange follows because the 2π rotation is equivalent to particle exchange.
proof idea
The declaration is a structure definition that introduces the twice field as an integer together with the nonnegativity constraint. No lemmas are applied and no tactics are used.
why it matters
This supplies the spin representation required by HasRSSpinorStructure and eight_tick_forces_D3, which establish that D=3 admits the RS spinor structure (two-component spinors, nonabelian simple Spin group). It realizes the spin-statistics link from the eight-tick phase mechanism and advances the T7 octave that forces D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.