alpha_s_two_loop_at_anchor

formal source

 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
 123structure TwoLoopAlphaSCert where
 124  /-- One-loop coefficient is positive at N_f = 5. -/
 125  b0_at5_pos : 0 < b0 5
 126  /-- Two-loop coefficient is positive at N_f = 5. -/
 127  b1_at5_pos : 0 < b1 5
 128  /-- The running formula reduces to identity at the anchor scale. -/
 129  reduces_at_anchor : ∀ (alpha_0 : ℝ) (N_f : ℕ) (mu_0_GeV : ℝ),
 130      0 < mu_0_GeV → alpha_s_two_loop alpha_0 N_f mu_0_GeV mu_0_GeV = alpha_0
 131
 132theorem twoLoopAlphaSCert_holds : TwoLoopAlphaSCert :=
 133  { b0_at5_pos := b0_at_Nf5_pos
 134    b1_at5_pos := b1_at_Nf5_pos
 135    reduces_at_anchor := alpha_s_two_loop_at_anchor }
 136
 137end
 138
 139end IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS