rotationPhase
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not use the period argument in its computation.
- Does not prove the numerical value -1 or +1.
- Applies only inside the discrete eight-tick phase model.
- Does not address continuous angles or higher-dimensional rotations.
Lean usage
theorem fermion_rotation_phase_neg_one : rotationPhase 4 = -1 := by unfold rotationPhase; exact phase_4_is_minus_oneformal statement (Lean)
39noncomputable def rotationPhase (period : ℕ) : ℂ :=
proof body
Definition body.
40 phaseExp ⟨4 % 8, by norm_num⟩
41
42/-- **KEY**: For fermions (4-tick period), the 2π rotation gives phase -1. -/