rs_alpha_s_anchor

formal source

  94def rs_anchor_scale : ℝ := 182.201  -- GeV
  95
  96/-- **RS α_s AT ANCHOR**: α_s(μ*) ≈ 0.1181. -/
  97def rs_alpha_s_anchor : ℝ := 0.1181
  98
  99/-- α_s at the anchor is positive and less than 1 (perturbative). -/
 100theorem rs_alpha_s_perturbative :
 101    0 < rs_alpha_s_anchor ∧ rs_alpha_s_anchor < 1 := by
 102  constructor <;> norm_num [rs_alpha_s_anchor]
 103
 104/-- **RS α_s(M_Z)**: Running from μ* = 182.201 GeV to M_Z = 91.2 GeV. -/
 105noncomputable def rs_alpha_s_MZ : ℝ :=
 106  alpha_s_running rs_alpha_s_anchor (b0_qcd 6) 91.2 rs_anchor_scale
 107
 108/-- The current one-loop RS value at `M_Z` stays in a perturbative range. -/
 109theorem rs_alpha_s_MZ_range :
 110    ∃ x : ℝ, rs_alpha_s_MZ = x ∧ 0.11 < x ∧ x < 0.14 := by
 111  refine ⟨rs_alpha_s_MZ, rfl, ?_, ?_⟩
 112  · unfold rs_alpha_s_MZ alpha_s_running rs_alpha_s_anchor rs_anchor_scale
 113    have hb0 : b0_qcd 6 = 7 := by
 114      norm_num [b0_qcd]
 115    rw [hb0]
 116    let denom : ℝ := 1 + (7 / (2 * Real.pi)) * 0.1181 * Real.log (91.2 / 182.201)
 117    have hratio_pos : 0 < (91.2 : ℝ) / 182.201 := by positivity
 118    have hratio_lt_one : (91.2 : ℝ) / 182.201 < 1 := by norm_num
 119    have hlog_neg : Real.log ((91.2 : ℝ) / 182.201) < 0 :=
 120      Real.log_neg hratio_pos hratio_lt_one
 121    have hcoeff_pos : 0 < (7 / (2 * Real.pi)) * 0.1181 := by positivity
 122    have hden_lt : denom < 1 := by
 123      dsimp [denom]
 124      nlinarith
 125    have hden_pos : 0 < denom := by
 126      have hlog_gt_neg_one : (-1 : ℝ) < Real.log ((91.2 : ℝ) / 182.201) := by
 127        rw [Real.lt_log_iff_exp_lt hratio_pos]