halfInt
plain-language theorem explainer
The halfInt constructor maps a natural number n to the Spin element whose twice-value equals n, thereby encoding the half-integer spin s = n/2. Researchers deriving the spin-statistics theorem from the eight-tick phase cycle cite this when instantiating explicit fermion and boson states. The definition is realized as a direct structure constructor whose non-negativity obligation is discharged by the omega tactic.
Claim. For each natural number $n$, the half-integer spin $s = n/2$ is the element of the Spin structure whose twice-value field equals $n$ together with a proof that $n$ is non-negative.
background
The SpinStatistics module derives the spin-statistics connection from Recognition Science's eight-tick phase accumulation. A 2π rotation traverses one full 8-tick cycle; half-integer spins accumulate a minus sign after two cycles while integer spins return to +1. The Spin structure stores twice the spin value as a non-negative integer to keep all arithmetic inside ℤ.
proof idea
The definition is a one-line wrapper that applies the Spin structure constructor to the pair (n, by omega).
why it matters
halfInt supplies the concrete spin states half and threeHalves that feed the phase mechanism of the spin-statistics derivation. It closes the interface between natural-number indexing and the integer twice-value required by the eight-tick cycle analysis, directly supporting the claim that odd n produces the fermion minus sign under 2π rotation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.