zero
plain-language theorem explainer
Zero spin is defined as the integer spin value 0 via the ofInt embedding into the Spin structure. Researchers deriving bosonic fields from the eight-tick phase cycle would cite this base case when constructing the integer spin ladder. The definition is a direct one-line wrapper applying the integer-to-spin constructor to zero.
Claim. The zero spin is the element of the Spin structure obtained by embedding the integer 0, so that twice the spin value equals 0 with the non-negativity witness holding.
background
The Spin structure encodes the spin quantum number as a half-integer n/2 for integer n, stored via the twice field in integers to preserve exact arithmetic together with a non-negativity proof. The ofInt constructor builds a Spin instance from a natural number n by setting twice to 2n and discharging the nonnegativity obligation via omega. This definition appears inside the QFT module whose module doc derives the spin-statistics theorem from phase accumulation over the 8-tick cycle, where integer spins accumulate phase +1 after one full cycle and correspond to bosons.
proof idea
The definition is a one-line wrapper that applies the ofInt constructor to the natural number 0, which in turn instantiates the Spin structure with twice equal to 0 and the nonnegativity witness generated automatically by omega.
why it matters
This supplies the base case for integer spins in the spin-statistics connection obtained from the eight-tick phase mechanism. It anchors the distinction between bosons (integer spin, symmetric statistics) and fermions (half-integer spin, antisymmetric statistics) that the module doc presents as emerging from 2π rotations traversing the 8-tick cycle. No downstream uses are recorded yet, but the definition closes the lowest rung of the spin ladder required for the phase formula exp(2πi s).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.