phaseExp
plain-language theorem explainer
phaseExp maps each index k in Fin 8 to the complex factor exp(i k π/4). Researchers on discrete symmetries and spin-statistics in Recognition Science cite it to obtain the 8th roots of unity. The definition is a direct one-line wrapper around Complex.exp applied to the real phase value.
Claim. For each $k=0,1,…,7$, define the complex phase factor $e_k := exp(i k π/4) ∈ ℂ$.
background
The module defines the 8-tick structure as the fundamental discrete clock of Recognition Science, with phases at 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. This cycle supplies the periodicity for spin-statistics (odd/even phase maps to fermion/boson), CPT symmetry, and gauge structure. The sibling definition phase supplies the real argument: phase(k) = k π/4 for k : Fin 8.
proof idea
The definition is a one-line wrapper that applies Complex.exp to (Complex.I * phase k), where phase is the sibling definition giving the real multiple of π/4.
why it matters
phaseExp supplies the complex values used by downstream results including phase_0_is_one, phase_4_is_minus_one, spin_statistics_key, eight_tick_generates_Z8, and sum_8_phases_eq_zero. It realizes the T7 eight-tick octave from the forcing chain and enables the Z/8Z symmetry that underlies vacuum cancellation and quantum ledger interference. The definition closes the link from the discrete clock to the roots-of-unity algebra required for particle statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.