vacuum_phase_one
plain-language theorem explainer
The phase exponential at the zero tick of the eight-cycle equals one, fixing the identity phase for the vacuum contribution. Researchers computing the electron anomalous magnetic moment from the Recognition Science ladder cite this identity to initialize the phase sum before adding Schwinger corrections. The proof is a direct one-line term application of the base case for tick zero.
Claim. Let phaseExp map each element $k$ of the eight-tick cycle to the complex value $e^{i phase(k)}$. Then phaseExp at the zero element equals 1.
background
The module derives the electron anomalous magnetic moment from the RS phi-ladder and the eight-tick octave. PhaseExp is the complex exponential of the phase function on Fin 8, so phaseExp(k) = exp(i * phase(k)). The upstream theorem phase_0_is_one states that the phase at k=0 gives 1 and is the identity phase with no change under exchange.
proof idea
The declaration is a one-line term-mode wrapper that directly applies the upstream theorem phase_0_is_one from the EightTick module.
why it matters
This identity initializes the vacuum phase for all subsequent anomalous-moment calculations in the module, including the eight-tick sum and Schwinger term. It supplies the T7 eight-tick octave starting point required by the Recognition Science forcing chain before the phi-ladder corrections are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.