pith. machine review for the scientific record. sign in
def definition def or abbrev high

two

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  76def two : Spin := ofInt 2

proof body

Definition body.

  77
  78/-- The actual spin value as a real number. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.