phaseQuantum
plain-language theorem explainer
The phase quantum is defined as π/4 radians, the base discrete phase step in the eight-tick cycle. Researchers modeling quantum anomalies via discrete time in QFT cite this unit when quantifying phase mismatches that break classical symmetries. The declaration is a direct noncomputable assignment with no lemmas or reduction steps.
Claim. The phase quantum equals $π/4$.
background
The QFT anomalies module derives anomalies from eight-tick phase mismatches between discrete and continuous phases. Upstream, EightTick.phase supplies the eight phases kπ/4 for k in Fin 8, with periodicity 2π. Wedge.phase converts a real phase w into the complex number e^{i w}. The module targets chiral anomalies such as π⁰ → γγ and conformal anomalies from the mismatch between the discrete eight-tick structure and continuous symmetries.
proof idea
The declaration is a direct definition that assigns π/4 to phaseQuantum, matching the phase increment from the eight-tick structure.
why it matters
This supplies the base unit for phase arithmetic throughout the anomalies module. It feeds eight_quanta_full_rotation, which proves eight quanta complete a 2π rotation, and AnomalyProofSummary, which records the eight-tick phase structure as a proven claim. The definition implements the T7 eight-tick octave landmark, enabling the paper's derivation of anomalies from discrete time structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.