full_cycle_identity
plain-language theorem explainer
Eight increments of the quantized phase per tick close exactly to a full 2π rotation. Researchers deriving chiral anomalies or conformal anomalies from discrete time would cite the identity to close phase cycles in 8-tick models. The proof is a one-line term that invokes the eight-quanta lemma directly.
Claim. $8$ times the phase increment per tick equals $2π$ in the discrete 8-tick cycle.
background
The module treats quantum anomalies as consequences of phase mismatches between continuous symmetries and an 8-tick discrete clock. Phase is the finite set of eight labels 0 through 7; each tick advances the phase by a fixed quantum whose eightfold sum recovers the full circle. Upstream results supply the cellular-automaton step that propagates the local rule and the Phase abbreviation that fixes the cycle length at eight.
proof idea
The proof is a one-line wrapper that applies the eight_quanta_full_rotation lemma.
why it matters
The identity closes the phase cycle required for anomaly calculations such as π⁰ → γγ. It realizes the eight-tick octave (T7) of the forcing chain and supplies the discrete-to-continuous bridge used in the QFT anomalies paper. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.