int_half_exclusive
plain-language theorem explainer
Integer and half-integer spin values are mutually exclusive. A researcher deriving the spin-statistics theorem from the eight-tick phase cycle would cite this to keep Bose and Fermi cases disjoint. The proof is a term-mode reduction that unfolds the two predicates and lets the omega tactic discharge the resulting integer contradiction.
Claim. For every spin quantum number $s$, it is not the case that $s$ is both an integer spin and a half-integer spin: $¬(isInteger(s) ∧ isHalfInteger(s))$.
background
The Spin structure represents the spin quantum number by an integer field twice (twice the spin value) together with a non-negativity guard, allowing exact representation of both integer and half-integer cases. The predicates isInteger and isHalfInteger are defined inside the Spin namespace to classify these values. This theorem lives in the QFT.SpinStatistics module whose module documentation states the goal of deriving the spin-statistics connection from phase accumulation over the 8-tick cycle.
proof idea
The proof unfolds isInteger and isHalfInteger, exposing their underlying integer-arithmetic definitions, then applies the omega tactic which automatically resolves the contradiction obtained from their conjunction.
why it matters
The lemma is invoked inside boson_symmetric_wavefunction and spin_statistics_boson to obtain an absurdity when a spin is assumed to satisfy both predicates simultaneously. It thereby supplies the required partition between integer (boson) and half-integer (fermion) classes before the 8-tick phase exp(2π i s) can assign symmetric or antisymmetric statistics. The result closes a logical prerequisite for the Recognition Science derivation of the spin-statistics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.