exchangePhase
plain-language theorem explainer
The exchangePhase definition assigns to each spin s the complex phase acquired under particle exchange, matching the phase from a 2π rotation via the 8-tick cycle. Researchers deriving the spin-statistics theorem from discrete time structures would cite this when linking rotation to exchange symmetry. It is realized as a direct one-line wrapper around cyclePhase.
Claim. For spin quantum number $s$, the exchange phase is $e^{2π i s}$, the phase factor acquired when two identical particles are exchanged, equivalent to the phase from one full $2π$ rotation.
background
The QFT.SpinStatistics module derives the spin-statistics theorem from Recognition Science's 8-tick structure, where one octave equals 8 ticks as the fundamental evolution period. The Spin structure holds twice the spin value as a nonnegative integer, distinguishing half-integer from integer cases. Upstream, cyclePhase computes the phase as Complex.exp(2 * π * I * s.value) over the 8-tick cycle, while tick sets the fundamental time quantum τ₀ = 1 and Phase is the Fin 8 space of discrete phases.
proof idea
This definition is a one-line wrapper that applies cyclePhase to the input spin s, returning the accumulated phase over one complete 8-tick cycle.
why it matters
This definition supplies the phase factor used in the downstream theorem exchange_equals_rotation, which establishes that half-integer spins yield phase -1 and integer spins yield +1 under exchange. It fills the phase accumulation step in the module's derivation of the spin-statistics theorem from the 8-tick octave. The result supports the framework's T7 eight-tick period and the equivalence of particle exchange with 2π rotation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.