alpha_s_two_loop_at_anchor
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.