int_or_half
plain-language theorem explainer
Every spin quantum number in the model is either integer or half-integer. Researchers deriving the spin-statistics theorem from the 8-tick phase cycle would cite this result to establish the fermion-boson partition. The proof unfolds the parity predicates on the doubled spin value and applies the omega tactic to resolve the integer disjunction.
Claim. For every spin quantum number $s$ (with integer representation $2s$), either $2s$ is even (integer spin) or $2s$ is odd (half-integer spin).
background
The Spin structure encodes the quantum number via an integer field twice (twice the spin value) together with the nonnegativity constraint twice ≥ 0. The predicates isInteger and isHalfInteger are defined directly on this field: isInteger holds when twice mod 2 = 0, while isHalfInteger holds when twice mod 2 = 1. The module QFT.SpinStatistics situates this dichotomy inside the derivation of the spin-statistics theorem from the 8-tick phase cycle, where a 2π rotation traverses one full cycle and half-integer spins require two cycles for closure.
proof idea
The term proof unfolds isInteger and isHalfInteger, exposing the parity conditions on the twice field, then invokes the omega tactic to discharge the resulting linear integer arithmetic disjunction.
why it matters
This result supplies the basic integer/half-integer partition required by the module's target derivation of spin-statistics from the 8-tick structure. It directly supports the phase mechanism in which odd twice yields the -1 factor for fermions and even twice yields +1 for bosons. The declaration aligns with the eight-tick octave (T7) in the forcing chain and prepares the ground for the antisymmetry argument under particle exchange.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.