b1_at_Nf5_pos
plain-language theorem explainer
The theorem establishes positivity of the two-loop beta coefficient b1 at five active quark flavors. QCD phenomenologists would cite it when confirming that asymptotic freedom holds in the two-loop running of alpha_s between the bottom and top thresholds. The proof is a direct specialization of the general low-N_f positivity result, with the bound N_f <= 8 discharged by a numerical check.
Claim. For five active quark flavors, the two-loop beta-function coefficient satisfies $b_1 > 0$, where $b_1(N_f) = (102 - 38 N_f / 3) / (8 pi^2)$.
background
The module derives the two-loop MS-bar running of the strong coupling alpha_s from the beta function d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3. Here b1 is the coefficient beta1 expressed in canonical SU(3) form as (102 - 38 N_f / 3) / (8 pi^2). The upstream lemma b1_pos_lowNf states that b1(N_f) > 0 whenever N_f <= 8, proved by unfolding the definition and applying linarith after casting the bound to reals.
proof idea
One-line wrapper that applies b1_pos_lowNf at N_f = 5, with the hypothesis 5 <= 8 discharged by norm_num.
why it matters
The result is packaged inside twoLoopAlphaSCert_holds to certify the two-loop formula at the anchor point. It closes the positivity requirement for the canonical N_f = 5 window in the module's extension of one-loop alpha_s running, preserving the sign that guarantees asymptotic freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.