phase_at_step
plain-language theorem explainer
The phase accumulated after k steps in the eight-tick cycle equals k times π over 4. Researchers modeling discrete-time symmetries or deriving anomalies in QFT would cite this to fix the phase quantum scale. The proof is a one-line algebraic reduction that unfolds the phase quantum definition and applies the ring tactic.
Claim. For every natural number $k$, the accumulated phase after $k$ steps satisfies $k · (π/4) = k π / 4$, where the phase quantum is defined to be $π/4$.
background
The QFT anomalies module derives quantum anomalies from mismatches between continuous phases and the discrete eight-tick structure. The eight-tick phase is defined as $k π / 4$ for $k = 0, …, 7$, so the phase quantum is exactly $π/4$. This theorem confirms linear phase accumulation per step before mismatch effects are introduced. Upstream, the EightTick.phase definition supplies the $k π / 4$ form, while phaseQuantum records the constant $π/4$ used throughout the module.
proof idea
The proof unfolds the definition of phaseQuantum (which equals $π/4$) and invokes the ring tactic to obtain the required equality.
why it matters
This anchors the phase quantization step that feeds derivations of chiral anomalies (e.g., π⁰ → γγ) in the same module. It realizes the eight-tick octave (T7) of the forcing chain, where the period-8 discreteness produces phase increments of $π/4$. The module doc-comment positions the result inside the paper proposition on quantum anomalies from discrete time structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.