int_or_half
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the phase accumulation rule that distinguishes fermions from bosons.
- Does not prove the full spin-statistics theorem.
- Does not incorporate the nonnegativity constraint into the parity claim.
- Does not link specific spin values to particles such as electrons or photons.
formal statement (Lean)
96theorem int_or_half (s : Spin) : s.isInteger ∨ s.isHalfInteger := by
proof body
Term-mode proof.
97 unfold isInteger isHalfInteger
98 omega
99
100/-- Integer and half-integer are mutually exclusive. -/