b0_at_Nf5_pos
plain-language theorem explainer
b0(5) > 0 holds for the one-loop beta coefficient in five-flavor QCD, securing the negative sign of the beta function and thus asymptotic freedom. QCD running analyses cite this when fixing the number of active flavors at the Z-pole. The term proof unfolds b0 and N_c then reduces via div_pos and norm_num.
Claim. $0 < b_0(5)$ where $b_0(N_f) := (11 N_c - 2 N_f)/(12 pi)$ and $N_c = 3$.
background
The Two-Loop QCD Running module extends one-loop alpha_s running by including the second beta-function coefficient b1 in the MS-bar scheme. The beta function is 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) for N_c = 3 colors. The upstream definition of b0 re-exports this canonical form directly from the AlphaRunning module.
proof idea
Unfolds b0 and N_c to obtain the explicit expression (33 - 10)/(12 pi). Applies the div_pos lemma to the positive denominator 12 pi (via the positivity tactic) and uses norm_num to confirm the numerator 23 is positive.
why it matters
Supplies the b0_at5_pos field inside TwoLoopAlphaSCert_holds that certifies the full two-loop running formula. It also feeds b0_pos_at5 in the MassAnomalousDimension module for the two-loop mass running ratio. This anchors asymptotic freedom at N_f = 5 in the Heavy Quark closure track, consistent with the beta-function sign required by the Recognition Science physics derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.