isHalfInteger
plain-language theorem explainer
The predicate isHalfInteger classifies a spin s as half-integer exactly when twice its value is odd. Researchers deriving spin-statistics relations from the 8-tick cycle cite it to separate fermions, which pick up a minus sign on 2π rotation, from bosons. The definition is a direct modular check on the twice field of the Spin structure with no auxiliary lemmas.
Claim. A spin quantum number $s$ is half-integer when $2s$ is odd, i.e., $2s mod 2 = 1$.
background
The QFT-001 module derives the spin-statistics theorem from Recognition Science's 8-tick phase structure. The Spin structure encodes the quantum number via its twice field (an integer twice the spin value) together with a nonnegativity guard. This predicate tests the parity of that field to mark fermions versus bosons. Upstream, the Spin structure supplies the integer representation that lets all later phase calculations stay inside ℤ arithmetic.
proof idea
Direct definition: the body computes s.twice % 2 and asserts equality to 1. No lemmas or tactics are invoked; it serves as the primitive classifier consumed by downstream results such as fermion_antisymmetric and exchange_equals_rotation.
why it matters
This definition supplies the classification step required by the module's core theorems, including electron_is_fermion (which asserts Spin.half satisfies the predicate) and exchange_equals_rotation (which routes half-integer spins to phase -1). It implements the T7 eight-tick octave landmark: odd multiples of the base tick produce the fermionic sign flip under a full cycle. The predicate therefore closes the discrete-time route to the spin-statistics connection and feeds Pauli-exclusion applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.