phase_alignment
plain-language theorem explainer
The declaration shows that the phase quantum multiplied by any multiple of eight equals an integer number of full 2π rotations. A physicist studying discrete-time effects in quantum field theory would cite it when analyzing phase quantization in the eight-tick model. The proof is a direct algebraic reduction that unfolds the phase quantum definition and normalizes the resulting expression with the ring tactic.
Claim. For every natural number $n$, $8n$ times the phase quantum equals $n$ times $2π$.
background
The QFT.Anomalies module derives quantum anomalies from mismatches between discrete 8-tick phases and continuous rotations. An anomaly arises when classical symmetry breaks under quantum effects, here traced to phase quantization introduced by the eight-tick discreteness. The phase quantum is the discrete phase increment per tick, with alignment occurring precisely at multiples of eight. Upstream structures include SpectralEmergence (forcing SU(3)×SU(2)×U(1) gauge content and 24 chiral fermions) and PhiForcingDerived (J-cost minimization), which supply the discrete foundation for the phase structure.
proof idea
The proof unfolds the definition of the phase quantum, applies push_cast to convert natural-number multiplication into reals, and invokes the ring tactic to confirm the algebraic identity.
why it matters
This result confirms the alignment condition that underpins the 8-tick phase mismatch mechanism for quantum anomalies. It directly supports the module's target of deriving anomalies from discrete time structure and connects to the eight-tick octave (T7) in the unified forcing chain. No downstream uses are recorded yet, and the declaration closes a basic consistency check rather than an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.