two
plain-language theorem explainer
Defines the spin-2 element in the Recognition Science Spin structure, representing the graviton. Researchers deriving the spin-statistics theorem from the eight-tick phase cycle cite this constant when building integer-spin boson cases. The definition is a direct one-line application of the integer constructor to the natural number 2.
Claim. The element of the Spin type with twice the value equal to 4, corresponding to the graviton quantum number $s=2$.
background
The Spin structure encodes quantum numbers as half-integers via an integer field twice together with a non-negativity guard; ofInt embeds a natural number n by setting twice to 2n. The module derives the spin-statistics connection from Recognition Science's eight-tick cycle: a 2π rotation traverses one full cycle, integer spins return to identity after one cycle while half-integer spins require two. Upstream, the ContinuumBridge supplies the simplicial-to-continuum identification used in the surrounding QFT development, and the RungFractions embedding supplies the rational ladder that hosts these spin values.
proof idea
One-line wrapper that applies ofInt to the natural number 2.
why it matters
Supplies the explicit spin-2 case required by the spin-statistics derivation in QFT-001, where integer spins accumulate phase +1 under the eight-tick cycle and therefore obey Bose-Einstein statistics. It is referenced by downstream action lemmas that establish geodesic minimizers and convex combinations of the J-cost functional, closing the loop from discrete phase rules to continuous variational principles. The declaration touches the T7 eight-tick octave landmark and the integer-spin branch of the spin-statistics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.