b0_pos_at5
plain-language theorem explainer
The one-loop beta coefficient remains positive at five active quark flavors, confirming asymptotic freedom for the QCD running coupling. Researchers deriving quark mass evolution and renormalization group flows cite this sign condition when proving positivity of mass ratios. The declaration is a direct one-line wrapper that invokes the already-proved positivity of b0 at N_f=5.
Claim. $0 < b_0(5)$ where $b_0(N_f) = (11N_c - 2N_f)/(12π)$ and $N_c=3$.
background
The module treats the two-loop MS-bar quark mass anomalous dimension and the associated running mass formula between scales μ and μ_0. The coefficient b0(N_f) is the one-loop beta-function term re-exported from the TwoLoopAlphaS module as b0(N_f) = (11N_c - 2N_f)/(12π). The upstream theorem b0_at_Nf5_pos already establishes that this expression is positive when N_f=5.
proof idea
One-line wrapper that directly applies the theorem b0_at_Nf5_pos.
why it matters
The result supplies the sign condition required by the sibling positivity theorems mass_ratio_leading_pos and mass_ratio_two_loop_pos inside the same module. It anchors the asymptotic-freedom property of the QCD beta function that underlies the closed-form mass running expressions derived from the Recognition Science RGE framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.