beta0_pos
plain-language theorem explainer
The result shows that the one-loop QCD beta-function coefficient stays positive whenever the number of active flavors does not exceed sixteen. QCD phenomenologists cite it to justify the ultraviolet freedom of the strong coupling at high energies. The short tactic script unfolds the explicit formula for b₀, invokes the positivity of division by a positive constant, and closes the inequality with linear arithmetic after casting the flavor bound to reals.
Claim. For any natural number $N_f$ satisfying $N_f ≤ 16$, the one-loop coefficient $b_0(N_f) = (11 N_c - 2 N_f)/(12 π)$ is strictly positive, where $N_c = 3$.
background
The module derives the running of the strong coupling α_s within Recognition Science by means of the one-loop beta function. The coefficient is defined by beta0(N_f) := (11 N_c - 2 N_f) / (12 π) where N_c = 3 is the number of colors. The local setting is the one-loop approximation to asymptotic freedom, with α_s fixed to 2/17 at the Z-boson mass.
proof idea
The proof unfolds the definition of beta0 together with N_c, then applies the lemma that a positive numerator divided by a positive denominator remains positive. It casts the hypothesis N_f ≤ 16 into reals and invokes nlinarith to confirm that 113 - 2N_f > 0 under the given bound.
why it matters
This positivity statement is invoked directly by the theorem asymptotic_freedom, which asserts that α_s grows stronger toward lower energies. It fills the chain step that guarantees the sign of b₀ for the physically relevant range N_f ≤ 16, consistent with the Recognition Science derivation of D = 3 and the eight-tick structure. No open questions are attached to this elementary positivity result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.