eight_quanta_full_rotation
plain-language theorem explainer
Eight discrete phases each advancing by π/4 sum to a full 2π rotation in the 8-tick cycle. Researchers deriving quantum anomalies from discrete time cite this identity when assembling phase-mismatch results. The proof is a one-line wrapper that unfolds the definitions of the phase count and phase increment then reduces the equality via the ring tactic.
Claim. $8 · (π/4) = 2π$, where 8 counts the discrete phases in one 8-tick cycle and π/4 is the phase quantum.
background
The QFT anomalies module derives anomalies from mismatches between continuous classical phases and the discrete 8-tick structure. Phase is the finite set Fin 8; one octave equals 8 ticks, the fundamental evolution period. numDiscretePhases is defined as the constant 8 and phaseQuantum as π/4. This rests on the tick definition τ₀ = 1 as the RS time quantum and on the Phase abbreviation as Fin 8 in the Church-Turing structure.
proof idea
The proof is a one-line wrapper. It unfolds numDiscretePhases and phaseQuantum, substituting the constants 8 and π/4, then applies the ring tactic to confirm the arithmetic identity.
why it matters
This supplies the rotation identity required by anomalyProofs, the summary collecting eight-tick rotation, pi0 lifetime accuracy, and related results. It fills the module's target proposition on anomalies from 8-tick phase mismatch and anchors the T7 eight-tick octave landmark by showing that eight quanta close the cycle. The identity is invoked directly by full_cycle_identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.