isInteger
plain-language theorem explainer
isInteger defines the predicate that identifies integer spin values, which correspond to bosons under the 8-tick phase accumulation rule. Researchers deriving the spin-statistics theorem from discrete time cycles cite this predicate to separate cases that acquire phase +1 from those acquiring phase -1. The definition is a direct modular check on the doubled spin coordinate.
Claim. Let $s$ be a spin quantum number represented by its doubled integer value $2s$. Then $s$ is an integer spin (boson) precisely when $2s$ is even, i.e., $2s$ is divisible by 2.
background
Spin is the structure recording a non-negative half-integer quantum number via the field twice : ℤ together with the proof twice ≥ 0. The predicate isInteger(s) holds exactly when twice(s) mod 2 = 0, which selects the integer values 0, 1, 2, … . The surrounding module QFT.SpinStatistics derives the spin-statistics connection from Recognition Science’s 8-tick cycle: a 2π rotation traverses one full cycle, integer spins return phase +1 after eight ticks while half-integer spins return phase -1 after sixteen ticks.
proof idea
One-line definition that directly unfolds to the arithmetic condition twice(s) % 2 = 0. The companion decidable instance is supplied by a simple if-then-else on the same modular test.
why it matters
The predicate feeds the parent theorems boson_symmetric, boson_symmetric_wavefunction and boson_symmetry_from_8tick, which establish that integer spins produce symmetric wavefunctions under the 8-tick cycle. It therefore supplies the integer half of the spin-statistics dichotomy required by the module’s target derivation of Bose-Einstein statistics from the eight-tick octave (T7). The definition closes the classification step that lets downstream results invoke the phase rule exp(2π i s) = +1 precisely when s is integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.