twoLoopAlphaSCert_holds
plain-language theorem explainer
The declaration certifies that the two-loop MS-bar running of the strong coupling obeys positivity of the one- and two-loop beta coefficients at five active flavors together with reduction to the input value at the anchor scale. A QCD phenomenologist matching alpha_s to lattice or collider data would invoke this certificate to justify the closed-form expression. The proof is a term-mode record construction that directly supplies the three required fields from the module's positivity and anchor lemmas.
Claim. The two-loop strong coupling satisfies $0 < b_0(5)$, $0 < b_1(5)$, and $1/alpha_s^{(2)}(alpha_0,N_f,mu_0,mu_0) = 1/alpha_0 + b_0 log(mu_0^2/mu_0^2) + (b_1/b_0) log(1 + b_0 alpha_0 log(mu_0^2/mu_0^2))$ reduces to the identity $alpha_s^{(2)}(alpha_0,N_f,mu_0,mu_0) = alpha_0$ whenever $mu_0 > 0$.
background
The module extends the one-loop alpha_s_running to the two-loop beta function in MS-bar: d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3 + O(alpha_s^4), with beta0 = (11 N_c - 2 N_f)/(12 pi) and beta1 = (102 - 38 N_f/3)/(8 pi^2) for SU(3). The closed form solved to two loops is 1/alpha_s(mu) = 1/alpha_s(mu_0) + beta0 log(mu^2/mu_0^2) + (beta1/beta0) log(1 + beta0 alpha_s(mu_0) log(mu^2/mu_0^2)). TwoLoopAlphaSCert is the structure requiring positivity of b0 and b1 at N_f=5 plus the anchor identity at mu=mu_0. Upstream results supply exactly these three ingredients: b0_at_Nf5_pos proves 0 < b0 5 by direct norm_num on the definition, b1_at_Nf5_pos chains through b1_pos_lowNf, and alpha_s_two_loop_at_anchor unfolds the running formula and cancels the log term via field_simp.
proof idea
The proof is a term-mode record construction of the TwoLoopAlphaSCert structure. It supplies the field b0_at5_pos directly from the lemma b0_at_Nf5_pos, b1_at5_pos from b1_at_Nf5_pos, and reduces_at_anchor from alpha_s_two_loop_at_anchor.
why it matters
This theorem completes the basic certification of the two-loop running formula inside the QCD RGE module and supplies the positivity and anchor properties required by the Heavy Quark closure track. It sits downstream of the one-loop AlphaRunning module. The result fills the two-loop extension step in the module's status of zero sorry statements and connects the standard QCD beta function to later threshold-matching work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.