two
plain-language theorem explainer
The definition supplies the concrete spin-2 element in the half-integer classification, standing for the graviton. Workers on the 8-tick derivation of spin-statistics or on integer-spin bosons would cite this instance. It is obtained by a direct call to the integer constructor on the natural number 2, which doubles the input and discharges non-negativity by omega.
Claim. Let $S$ be the structure whose elements are pairs $(k, p)$ with $k$ a non-negative integer and $p$ a proof that $k$ is non-negative; the spin value is then $k/2$. The element $s_2$ is the member of $S$ obtained by feeding the natural number 2 into the integer constructor, yielding $k=4$.
background
The Spin structure records quantum numbers as half-integers by storing twice the value in an integer field together with a non-negativity witness. The ofInt map turns a natural number $n$ into the element whose twice field equals $2n$. The surrounding module derives the spin-statistics link from the 8-tick phase cycle: a $2π$ rotation traverses one full cycle, integer spins return phase $+1$ after one cycle, and half-integer spins return $-1$ after two cycles.
proof idea
One-line definition that applies the ofInt constructor to the natural number 2; the resulting structure literal is accepted because omega discharges the non-negativity obligation on the twice field.
why it matters
The instance populates the integer-spin side of the spin-statistics theorem obtained from the 8-tick phase mechanism and is referenced by downstream results on geodesic equations and convexity of the J-cost functional. It therefore supplies the concrete boson case (phase $+1$ after one 8-tick cycle) required by the T7 octave and the overall Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.