alpha_s_two_loop_at_anchor
The theorem shows that the two-loop QCD running coupling returns exactly to its input value alpha_0 when the renormalization scale equals the reference scale mu_0. QCD phenomenologists anchoring alpha_s at a physical point such as m_Z invoke this identity to initialize the evolution. The proof is a short tactic sequence that unfolds the closed-form expression, cancels the scale ratio inside the logarithm, and simplifies the denominator to unity.
claimLet alpha_0 be real, N_f a natural number, and mu_0 > 0. Then the two-loop strong coupling in the MS-bar scheme satisfies alpha_s^{(2)}(mu_0; alpha_0, N_f) = alpha_0.
background
The module solves the two-loop beta-function equation for the strong coupling alpha_s in the MS-bar scheme. The closed-form expression alpha_s_two_loop is defined by dividing alpha_0 by a denominator that contains the one-loop term b0 alpha_0 L together with the two-loop correction (b1/b0) alpha_0 log(1 + b0 alpha_0 L), where L = log(mu^2/mu_0^2). The local theoretical setting is SU(3) QCD with N_f active flavors and no threshold matching. The upstream definition alpha_s_two_loop supplies the explicit formula whose special case at equal scales is proved here.
proof idea
Unfold the definition of alpha_s_two_loop. Use positivity of mu_0 to prove that mu_0^2/mu_0^2 equals 1, replace the logarithm by log 1 = 0, and simplify the resulting expression to alpha_0.
why it matters in Recognition Science
The result supplies the reduces_at_anchor field inside twoLoopAlphaSCert_holds, which constructs the master certificate TwoLoopAlphaSCert. It confirms consistency of the closed-form solution at the reference point and supports the Heavy Quark closure track. The identity aligns with the Recognition Science treatment of running parameters derived from the J-function and phi-ladder.
scope and limits
- Does not derive the beta-function coefficients b0 and b1.
- Does not incorporate heavy-quark threshold matching.
- Does not extend the running to three loops or higher.
- Does not constrain the numerical values of N_f or alpha_0.
Lean usage
have h_anchor : alpha_s_two_loop alpha_0 N_f mu_0 mu_0 = alpha_0 := alpha_s_two_loop_at_anchor alpha_0 N_f mu_0 h_mu_posformal statement (Lean)
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
proof body
Tactic-mode proof.
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