twoLoopAlphaSCert_holds
plain-language theorem explainer
The theorem certifies that the two-loop MS-bar running formula for the strong coupling satisfies positivity of the one- and two-loop beta-function coefficients at five active flavors together with reduction to the identity at the reference scale. QCD phenomenologists would cite it to justify the closed-form evolution inside heavy-quark threshold calculations. The proof is a direct term-mode construction that populates the three fields of the required certification structure from the three sibling lemmas on positivity and the anchor identity.
Claim. Let $b_0(N_f)$ and $b_1(N_f)$ be the standard one- and two-loop coefficients of the QCD beta function in the MS-bar scheme. Then $b_0(5)>0$, $b_1(5)>0$, and the two-loop running formula satisfies $1/alpha_s(mu)=1/alpha_s(mu_0)+b_0 log(mu^2/mu_0^2)+(b_1/b_0)log(1+b_0 alpha_s(mu_0)log(mu^2/mu_0^2))$ with the property that $alpha_s(alpha_0,N_f,mu_0,mu_0)=alpha_0$ for all $mu_0>0$.
background
The module supplies the two-loop extension of the strong-coupling running in the MS-bar scheme. The beta function takes the form $d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3 + O(alpha_s^4)$, with beta0 = (11 Nc - 2 Nf)/(12 pi) and beta1 = (102 - 38 Nf/3)/(8 pi^2) for Nc=3. The closed-form solution is obtained by direct integration and yields the explicit expression quoted above. The certification structure requires three concrete properties: positivity of b0 at Nf=5, positivity of b1 at Nf=5, and exact reduction of the running formula to the identity at the anchor scale mu=mu0.
proof idea
The proof is a term-mode construction. It directly supplies the three fields of the certification structure by referencing the sibling lemmas b0_at_Nf5_pos, b1_at_Nf5_pos and alpha_s_two_loop_at_anchor.
why it matters
This declaration certifies the two-loop running formula that forms Module 1 of the Heavy Quark closure track. It supplies the positivity and anchor properties demanded by the certification structure, thereby closing the two-loop extension of the existing one-loop running without axioms or sorrys. The result supports subsequent threshold-matching steps in the same track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.