sum_8_phases_eq_zero
plain-language theorem explainer
The sum of the eight complex exponentials of the discrete phases vanishes identically. Quantum field theorists and vacuum fluctuation modelers cite the result to establish destructive interference of vacuum modes. The proof identifies each phaseExp k with a power of a primitive eighth root of unity and invokes the standard geometric-sum identity for roots of unity.
Claim. Let $ζ = exp(i π / 4)$. Then $∑_{k=0}^{7} exp(i k π / 4) = 0$.
background
The module defines the 8-tick phases by phase(k) = k π / 4 for k : Fin 8 and the complex exponential phaseExp(k) = exp(i · phase(k)). These phases realize the discrete clock whose period is 2³ ticks and whose even/odd parity distinguishes bosons from fermions. The local setting is the 8-tick structure that underlies spin-statistics, CPT symmetry and gauge-group emergence. The proof depends on the definitions of phase and phaseExp together with the primitive-root lemma Complex.isPrimitiveRoot_exp.
proof idea
The tactic proof first constructs ζ = exp(2 π i / 8) and proves it is a primitive eighth root via Complex.isPrimitiveRoot_exp. It then shows phaseExp k = ζ^k by unfolding the definitions and applying exp_nat_mul together with ring. The sum is rewritten as a range sum via Fin.sum_univ_eq_sum_range, after which the primitive-root geometric-sum theorem yields zero.
why it matters
The theorem supplies the algebraic engine for vacuum fluctuation cancellation and is invoked directly by eight_tick_interference in QuantumLedger, vacuum_fluctuation_cancellation in SpinStatistics, and the corresponding cancellation theorems in VacuumFluctuations. It realizes the eight-tick octave (T7) of the forcing chain and furnishes the root-of-unity identity required for the boson/fermion phase distinction. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.