rotationPhase
plain-language theorem explainer
rotationPhase defines the complex phase acquired under a 2π rotation in the eight-tick model by evaluating phaseExp at index 4. Researchers deriving exchange symmetries in Recognition Science cite it when connecting rotation to particle statistics. The definition is a direct one-line application of the upstream phaseExp constructor to the fixed four-tick index.
Claim. The phase accumulated under a 2π rotation is given by rotationPhase(period) := phaseExp(4 mod 8), where phaseExp(k) = exp(i k π / 4) for k ∈ {0,…,7}.
background
The SpinStatistics module derives the spin-statistics theorem from the RS eight-tick ledger. Upstream, phase(k : Fin 8) := (k : ℝ) * π / 4 and phaseExp(k) := exp(I * phase k), with the property that each eighth power equals 1. The module doc states that four-tick states acquire phase -1 under 2π rotation while eight-tick states return to themselves, forcing antisymmetry or symmetry under exchange.
proof idea
One-line definition that applies phaseExp to the Fin 8 index 4 (via 4 % 8). It relies directly on the phaseExp and phase definitions from Foundation.EightTick.
why it matters
This supplies the concrete rotation phase used by fermion_rotation_phase_neg_one and exchange_sign_fermion, which establish the full spin_statistics_theorem. It instantiates the eight-tick octave (T7) for the fermion case in the RS derivation of the spin-statistics connection, as required by RS_Spin_Statistics_Theorem.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.