def
definition
rs_counter_term
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Experimental.MuonGMinusTwo on GitHub at line 53.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
50 · nlinarith [phi_pos]
51
52/-- The RS counter-term for muon g-2. -/
53noncomputable def rs_counter_term : ℝ :=
54 (alpha_em / Real.pi) * (phi ^ (-muon_rung)) * gap_1332_factor
55
56/-- **THEOREM EA-001.4**: The RS counter-term is positive. -/
57theorem rs_counter_positive : rs_counter_term > 0 := by
58 unfold rs_counter_term
59 have h0 : 0 < alpha_em / Real.pi := by
60 unfold alpha_em
61 apply div_pos
62 · norm_num
63 · positivity
64 have h1 : 0 < phi ^ (-muon_rung : ℝ) := by
65 apply Real.rpow_pos_of_pos
66 exact phi_pos
67 have h2 : 0 < gap_1332_factor := gap_factor_pos
68 have h3 : 0 < (alpha_em / Real.pi) * (phi ^ (-muon_rung : ℝ)) := mul_pos h0 h1
69 exact mul_pos h3 h2
70
71/-! ## III. The RS Prediction -/
72
73/-- The SM reference point used here: Schwinger + hadronic seed. -/
74noncomputable def sm_reference : ℝ := schwinger_term + 0.000711317
75
76/-- The RS prediction for muon g-2. -/
77noncomputable def a_mu_rs_prediction : ℝ :=
78 sm_reference + rs_counter_term
79
80/-- **THEOREM EA-001.5**: The RS prediction exceeds SM prediction. -/
81theorem rs_exceeds_sm : a_mu_rs_prediction > sm_reference := by
82 unfold a_mu_rs_prediction
83 linarith [rs_counter_positive]