b0_sm_positive
plain-language theorem explainer
The one-loop QCD beta-function coefficient evaluates to seven for six active quark flavors, confirming the positive sign required for asymptotic freedom in the Standard Model. Particle physicists studying renormalization-group flows would cite this when checking the ultraviolet behavior of the strong coupling. The proof is a direct algebraic substitution into the closed-form expression for the coefficient followed by numerical verification of the inequality.
Claim. For the Standard Model with six quark flavors, the one-loop coefficient satisfies $b_0 = 11 - 2n_f/3 > 0$ at $n_f=6$.
background
The module derives renormalization-group running from the Recognition Science φ-ladder. The beta function arises as the ladder derivative of the coupling, β(g) = (1/ln φ) dg/dr. The coefficient b0_qcd(n_f) is defined by the explicit formula 11 - 2 n_f /3, which fixes the sign of β for SU(3) gauge theory and thereby controls asymptotic freedom when n_f < 16.5. This theorem specializes the general expression to the Standard Model quark content n_f = 6. The upstream definition of b0_qcd supplies the arithmetic expression evaluated here.
proof idea
The proof unfolds the definition of b0_qcd at argument 6 to obtain the arithmetic expression 11 - 4 and applies norm_num to confirm that the result is strictly positive.
why it matters
This result confirms asymptotic freedom for the Standard Model inside the RS framework and supports the module-level claim that β_QCD < 0 for n_f ≤ 16. It sits downstream of the φ-ladder derivative structure and feeds the broader asymptotic-freedom criterion. The computation aligns with the forced eight-tick octave and three spatial dimensions that fix the gauge-group content in the foundational chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.