b1_pos_lowNf
plain-language theorem explainer
b1_pos_lowNf shows that the two-loop beta coefficient b1 stays positive for every natural number N_f at most 8. QCD phenomenologists cite the result when confirming that asymptotic freedom survives through the light-quark thresholds in the MS-bar scheme. The argument substitutes the closed-form expression for b1 and resolves the resulting real inequality by linear arithmetic after a cast.
Claim. For every natural number $N_f$ with $N_f ≤ 8$, the two-loop coefficient satisfies $b_1(N_f) > 0$, where $b_1(N_f) = (102 - 38 N_f / 3) / (8 π^2)$.
background
The module extends the one-loop alpha_s running to two loops in the MS-bar scheme for QCD with N_c = 3. The coefficient b1 is defined by the standard expression (102 - 38 N_f / 3) / (8 π^2). The module documentation records the two-loop running formula 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)) and states that the present lemma supplies the required positivity for N_f ≤ 8.
proof idea
Unfold the definition of b1. Apply div_pos to the positive denominator 8 π^2. Cast the hypothesis N_f ≤ 8 into a real-number inequality via exact_mod_cast. Finish with linarith on the resulting linear inequality.
why it matters
The lemma is invoked directly by the downstream instance b1_at_Nf5_pos at the canonical five-flavor point. It thereby anchors the sign of the two-loop correction inside the QCD RGE module before threshold matching is treated. The module documentation notes that this step closes the basic positivity properties needed for the two-loop running formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.