boson_phase_from_foundation
plain-language theorem explainer
The theorem states that the phase factor at tick zero in the eight-tick cycle equals one, supplying the symmetric exchange phase required for bosons. Workers deriving spin-statistics from discrete time foundations cite this result to anchor Bose-Einstein statistics in the proven eight-tick structure. The proof is a one-line wrapper that applies the phase_0_is_one lemma from the EightTick foundation.
Claim. In the eight-tick phase structure, the phase exponential at tick zero satisfies $phaseExp(0) = 1$, which is the identity phase under exchange for integer-spin particles.
background
The QFT.SpinStatistics module derives the spin-statistics theorem from Recognition Science's eight-tick cycle. A 2π rotation traverses one full cycle of eight ticks; integer spin returns to the same state after one cycle (phase +1, bosons) while half-integer spin requires two cycles (phase -1, fermions). The phase mechanism follows from the Recognition Composition Law and the eight-tick octave (T7).
proof idea
The proof is a one-line wrapper that directly invokes the upstream theorem phase_0_is_one from Foundation.EightTick, whose own proof unfolds phaseExp and simplifies the exponential at argument zero to yield 1.
why it matters
This supplies the boson component of the unified spin-statistics result and is invoked by the parent theorem spin_statistics_from_foundation, which combines it with the fermion phase at tick 4 and the sum of all eight phases equaling zero. It completes the foundation connection step in the QFT-001 derivation, grounding Bose-Einstein statistics in the eight-tick octave rather than postulating it. The result touches the T7 landmark in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.