boson_symmetric
plain-language theorem explainer
Integer spin particles acquire a phase factor of +1 after one full 8-tick cycle. Researchers deriving spin-statistics from discrete time structures cite this to establish the bosonic case before handling fermions. The proof extracts an integer k from the even twice-spin value, rewrites the phase as an integer multiple of 2πi, and invokes the standard complex exponential identity.
Claim. Let $s$ be a spin quantum number that is an integer. Then the phase factor acquired under the full 8-tick cycle equals $1$.
background
The Spin structure records the quantum number via an integer twice its value to keep arithmetic exact, with the isInteger predicate holding exactly when that twice-value is even. The cyclePhase function returns the complex phase exp(2πi s) accumulated when the particle completes the 8-tick cycle, which the module identifies with a 2π rotation. This theorem belongs to the module that extracts the spin-statistics connection from the 8-tick phase mechanism, where integer spins close with +1 while half-integer spins close with -1. The upstream phase definition supplies the eight discrete phases as multiples of π/4.
proof idea
The tactic proof unfolds cyclePhase together with the integer-spin predicate. It obtains an integer k such that twice-spin equals 2k from the evenness hypothesis. The phase expression is algebraically rewritten to equal k times 2πi, after which the identity exp(2πi k) = 1 is applied.
why it matters
This supplies the bosonic phase factor required by the downstream theorem boson_symmetry_from_8tick, which concludes that the wavefunction is unchanged under exchange. It likewise supports exchange_equals_rotation by furnishing the +1 case. In the Recognition Science framework it realizes the integer-spin branch of the eight-tick octave, confirming that bosons close after one cycle. The result closes one concrete step in the QFT-001 program for obtaining spin-statistics from the discrete time structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.