ofInt
ofInt maps each natural number n to an integer spin s = n by storing twice that value in the Spin structure. Researchers deriving spin-statistics from the eight-tick phase cycle cite it when assembling boson states such as photons or gravitons. The definition is a direct structure constructor whose non-negativity obligation is discharged by a single arithmetic check.
claimThe map sends each natural number $n$ to the spin quantum number $s$ with $2s = 2n$ and $s$ non-negative.
background
Spin is the structure that encodes the spin quantum number as a half-integer, stored internally as an integer twice the value together with a proof that the stored integer is non-negative. The QFT.SpinStatistics module derives the spin-statistics theorem from Recognition Science's eight-tick cycle: a $2π$ rotation traverses one full cycle, integer spins return to the identity after one cycle while half-integer spins require two. Upstream, the half definition in the same module and the RungFractions.ofInt embedding supply the complementary half-integer and rung constructions used alongside this integer case.
proof idea
The definition is a one-line wrapper that applies the Spin constructor to the pair consisting of twice the input natural number and the non-negativity proof generated by the omega tactic.
why it matters in Recognition Science
This constructor supplies the integer-spin cases required by the zero, one, and two definitions that appear later in the module; those definitions in turn feed the phase-accumulation argument that distinguishes bosons from fermions under the eight-tick octave. It therefore occupies the integer rung of the spin ladder complementary to the half-integer cases, directly supporting the T7 eight-tick structure and the spin-statistics connection claimed in the module header.
scope and limits
- Does not construct half-integer spins.
- Does not derive the spin-statistics theorem.
- Does not encode the phase accumulation rule exp(2πis).
- Does not reference the phi-ladder or mass formulas.
Lean usage
def zero : Spin := ofInt 0formal statement (Lean)
58def ofInt (n : ℕ) : Spin := ⟨2 * n, by omega⟩
proof body
Definition body.
59
60/-- Create a half-integer spin (s = n/2). -/