alpha_s_running

formal source

  79
  80/-- **ONE-LOOP RUNNING α_s**:
  81    α_s(μ) = α_s(μ*) / (1 + b₀/(2π) × α_s(μ*) × ln(μ/μ*)) -/
  82noncomputable def alpha_s_running (α_s_anchor b₀ μ μ_star : ℝ) : ℝ :=
  83  α_s_anchor / (1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star))
  84
  85/-- α_s is positive when denominator is positive. -/
  86theorem alpha_s_positive (α_s_anchor b₀ μ μ_star : ℝ)
  87    (hα : 0 < α_s_anchor)
  88    (hdenom : 0 < 1 + b₀ / (2 * Real.pi) * α_s_anchor * Real.log (μ / μ_star)) :
  89    0 < alpha_s_running α_s_anchor b₀ μ μ_star := by
  90  unfold alpha_s_running
  91  exact div_pos hα hdenom
  92
  93/-- **RS ANCHOR SCALE**: μ* = 182.201 GeV (stationarity point of RG). -/
  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