exchange_sign_boson
plain-language theorem explainer
The bosonic exchange phase factor in the eight-tick model squares to unity, confirming symmetric statistics under particle exchange. Researchers deriving Bose-Einstein condensation or integer-spin behavior from discrete RS phases would cite this when closing the bosonic sector of the spin-statistics connection. The proof substitutes the zero-tick identity lemma and reduces the product by ring.
Claim. Let $p_0$ denote the phase factor at zero ticks in the eight-tick cycle. Then $p_0^2 = 1$.
background
The module derives the spin-statistics theorem from the RS eight-tick ledger. It defines phase(k) for k in Fin 8 as kπ/4 and phaseExp as the associated complex exponential. The zero-tick case supplies the identity phase for bosons, while the four-tick case supplies the sign flip for fermions. Upstream, phase_0_is_one states that phaseExp at zero equals 1 and is described as the identity phase with no change under exchange. The local setting is the eight-tick octave that forces D=3 spatial dimensions and the full spin-statistics link.
proof idea
One-line wrapper that applies phase_0_is_one to replace both factors by 1, then invokes ring to obtain the product identity.
why it matters
This declaration supplies the bosonic half of the spin-statistics theorem. It feeds the parent result spin_statistics_theorem and is certified by spin_statistics_key in Foundation.EightTick. The result aligns with the eight-tick octave (T7) and the distinction between 4-tick fermions and 8-tick bosons. It closes one concrete case in the paper RS_Spin_Statistics_Theorem.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.