b1_at_Nf5_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit integrated two-loop solution for alpha_s(mu).
- Does not treat quark-mass threshold matching.
- Does not establish positivity for N_f > 8.
- Does not address higher-loop coefficients.
Lean usage
theorem twoLoopAlphaSCert_holds : TwoLoopAlphaSCert := { b0_at5_pos := b0_at_Nf5_pos, b1_at5_pos := b1_at_Nf5_pos, reduces_at_anchor := alpha_s_two_loop_at_anchor }formal statement (Lean)
61theorem b1_at_Nf5_pos : 0 < b1 5 := b1_pos_lowNf 5 (by norm_num)
proof body
Term-mode proof.
62
63/-- One-loop coefficient at N_f = 5 is positive (asymptotic freedom). -/