one
plain-language theorem explainer
This definition embeds the integer 1 into the Spin structure to represent spin-1 bosons such as the photon. Researchers deriving spin-statistics from the 8-tick cycle or proving convexity and rigidity of J-cost actions cite it when instantiating integer-spin cases. The construction is a direct one-line wrapper that applies the ofInt map to the natural number 1.
Claim. The integer spin quantum number $s=1$ is the element of the Spin structure whose twice-value field equals 2, obtained by applying the integer embedding map to 1.
background
The Spin structure stores twice the spin value as a non-negative integer to support integer arithmetic for both integer and half-integer cases. The ofInt function constructs integer spins by doubling the input natural number and discharging the nonnegativity obligation. This sits inside the QFT module whose module doc derives the spin-statistics theorem from phase accumulation over the 8-tick cycle: integer spins return phase +1 after one cycle while half-integer spins return -1 after two cycles.
proof idea
The definition is a direct constructor application of ofInt to the natural number 1, with the nonnegativity proof supplied automatically by the omega tactic inside ofInt.
why it matters
It supplies the concrete spin-1 instance required by downstream results such as costRateEL_implies_const_one (rigidity of constant paths at the J-cost minimum) and actionJ_convex_on_interp (convexity of the action functional). The definition instantiates the integer-spin slot in the 8-tick phase mechanism for the spin-statistics theorem, directly supporting the eight-tick octave landmark and the emergence of Bose-Einstein statistics for bosons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.