def
definition
phaseQuantum
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.QFT.Anomalies on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
38def numDiscretePhases : ℕ := 8
39
40/-- Phase quantum (2π/8 = π/4). -/
41noncomputable def phaseQuantum : ℝ := π / 4
42
43/-- **THEOREM**: 8 phase quanta make a full rotation. -/
44theorem eight_quanta_full_rotation :
45 (numDiscretePhases : ℝ) * phaseQuantum = 2 * π := by
46 unfold numDiscretePhases phaseQuantum
47 ring
48
49/-- **THEOREM**: Phase after k steps in the 8-tick cycle. -/
50theorem phase_at_step (k : ℕ) :
51 (k : ℝ) * phaseQuantum = k * π / 4 := by
52 unfold phaseQuantum
53 ring
54
55/-- **THEOREM**: After 8 steps, return to identity (phase = 2π). -/
56theorem full_cycle_identity :
57 (8 : ℕ) * phaseQuantum = 2 * π := eight_quanta_full_rotation
58
59/-- **THEOREM**: Phase at step 4 is π (half rotation = sign flip). -/
60theorem half_cycle_phase :
61 (4 : ℕ) * phaseQuantum = π := by
62 unfold phaseQuantum
63 ring
64
65/-! ## The π⁰ → γγ Decay Prediction -/
66
67/-- Predicted π⁰ lifetime from the anomaly (in units of 10⁻¹⁷ seconds). -/
68def pi0_lifetime_predicted_units : ℚ := 84/10 -- 8.4 × 10⁻¹⁷ s
69
70/-- Observed π⁰ lifetime (in units of 10⁻¹⁷ seconds). -/
71def pi0_lifetime_observed_units : ℚ := 852/100 -- 8.52 × 10⁻¹⁷ s