rotationPhase
plain-language theorem explainer
rotationPhase supplies the complex phase factor for a 4-tick advance under 2π rotation. Quantum field theorists deriving spin-statistics relations in Recognition Science cite this when establishing fermion exchange signs. The definition is realized as a one-line wrapper that feeds the fixed index 4 into phaseExp from the eight-tick cycle.
Claim. The phase factor for the 4-tick fermion rotation is given by the complex exponential at the fourth position of the eight-tick sequence, yielding $e^{iπ} = -1$.
background
The Spin-Statistics module builds the spin-statistics connection from the eight-tick ledger. The phase function returns the real angle $kπ/4$ for $k$ in Fin 8, while phaseExp returns the unit complex number $e^{i k π/4}$. The tick is the fundamental RS time quantum normalized to 1. Upstream results record that each phaseExp value raised to the eighth power equals 1, confirming periodicity after one octave.
proof idea
The definition is a one-line wrapper that applies phaseExp to the index 4 modulo 8.
why it matters
This definition supplies the rotation phase that enters exchange_sign_fermion and fermion_rotation_phase_neg_one. Those results support spin_statistics_theorem, which equates exchange sign to rotation phase, and pauli_exclusion. It fills the central step in the RS spin-statistics theorem from RS_Spin_Statistics_Theorem.tex and connects directly to the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.