eight_tick_sum
plain-language theorem explainer
The sum of eight complex phase exponentials from the eight-tick structure equals zero. Researchers deriving the electron anomalous magnetic moment via the RS φ-ladder would cite this to establish vacuum fluctuation cancellation. The proof is a one-line wrapper that invokes the roots-of-unity summation theorem.
Claim. $∑_{k=0}^{7} exp(i k π/4) = 0$, where the terms are the eighth roots of unity.
background
The module derives the electron anomalous magnetic moment from the RS φ-ladder, following the paper RS_Electron_g_minus_2.tex. It imports the eight-tick foundation to handle phase sums that cancel vacuum contributions to the g-factor. phaseExp(k) is the complex exponential exp(I * phase(k)) for each tick k in Fin 8. The upstream theorem sum_8_phases_eq_zero states that the sum of all eight phases equals zero because they are the eighth roots of unity, providing the foundation of vacuum fluctuation cancellation.
proof idea
The proof is a one-line wrapper that applies the sum_8_phases_eq_zero theorem from the EightTick module.
why it matters
This result instantiates the eight-tick octave (T7) in the forcing chain and supplies the cancellation property required for the Schwinger term a_e^(1) = α/(2π). It feeds the sibling derivations of the electron g-factor and the leading anomalous moment. The declaration closes the vacuum-phase step in the RS derivation of the alpha band without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.