alpha_s_two_loop_pos_when_denom_pos

formal source

  89/-- Positivity of the two-loop alpha_s under the MS-bar perturbative window:
  90    when the alpha_0 input is positive and the log scale ratio is bounded
  91    so the denominator stays positive, the running coupling is positive. -/
  92theorem alpha_s_two_loop_pos_when_denom_pos
  93    (alpha_0 : ℝ) (N_f : ℕ) (mu_GeV mu_0_GeV : ℝ)
  94    (h_alpha_pos : 0 < alpha_0)
  95    (h_denom_pos : 0 < 1 + b0 N_f * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) +
  96                    (b1 N_f / b0 N_f) * alpha_0 *
  97                    Real.log (1 + b0 N_f * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2))) :
  98    0 < alpha_s_two_loop alpha_0 N_f mu_GeV mu_0_GeV := by
  99  unfold alpha_s_two_loop
 100  exact div_pos h_alpha_pos h_denom_pos
 101
 102/-! ## At-Z bracket sanity check
 103
 104The PDG value `alpha_s(M_Z) = 0.1179 +- 0.0009`. The RS prediction is
 105`alpha_s_geom = 2/17 ≈ 0.11765`, sitting inside the PDG bracket. The two-loop
 106formula, evaluated at mu_0 = M_Z = mu, returns alpha_0 exactly (the log
 107vanishes), so the two-loop framework is self-consistent at the anchor scale.
 108-/
 109
 110/-- At `mu = mu_0`, the running coupling equals the input coupling. -/
 111theorem alpha_s_two_loop_at_anchor (alpha_0 : ℝ) (N_f : ℕ) (mu_0_GeV : ℝ)
 112    (h_mu_pos : 0 < mu_0_GeV) :
 113    alpha_s_two_loop alpha_0 N_f mu_0_GeV mu_0_GeV = alpha_0 := by
 114  unfold alpha_s_two_loop
 115  have h1 : mu_0_GeV ^ 2 / mu_0_GeV ^ 2 = 1 := by
 116    have h_sq : 0 < mu_0_GeV ^ 2 := pow_pos h_mu_pos 2
 117    field_simp
 118  rw [h1, Real.log_one]
 119  simp
 120
 121/-! ## Master cert -/
 122