phase_alignment
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit numerical value of the phase quantum.
- Does not prove misalignment for step counts not divisible by eight.
- Does not derive coefficients for specific anomalies such as the chiral anomaly.
- Does not extend the identity to continuous or non-integer time steps.
formal statement (Lean)
186theorem phase_alignment (n : ℕ) :
187 (8 * n : ℕ) * phaseQuantum = n * (2 * π) := by
proof body
Term-mode proof.
188 unfold phaseQuantum
189 push_cast
190 ring
191
192/-- **THEOREM**: Phases are misaligned for non-multiples of 8. -/