beta0_at_Z
plain-language theorem explainer
The one-loop beta-function coefficient evaluates to 23/(12π) once the number of active flavors is fixed at five. QCD running calculations that start from the RS value α_s(M_Z) = 2/17 cite this numerical coefficient when evolving the coupling to lower scales. The proof substitutes the constants N_c = 3 and N_f_Z = 5 into the general beta0 definition and normalizes the arithmetic expression.
Claim. $b_0(N_f=5) = 23/(12π)$, where the one-loop coefficient is given by $b_0(N_f) = (11N_c - 2N_f)/(12π)$ with $N_c = 3$.
background
The module computes the running of the strong coupling α_s from the Recognition Science input α_s(M_Z) = 2/17 using the one-loop beta function. The coefficient b0 is defined by the standard QCD expression (11N_c - 2N_f)/(12π) and is positive for N_f < 17, which encodes asymptotic freedom. N_c is fixed at three colors and N_f_Z at five active flavors below the Z-pole mass.
proof idea
One-line wrapper that unfolds the definitions of beta0, N_c and N_f_Z, then applies the ring tactic to reduce the resulting rational expression to 23/(12π).
why it matters
It supplies the concrete numerical value of b0 at the Z scale that enters every subsequent one-loop running formula in the module. The module doc-comment states that this b0 > 0 guarantees asymptotic freedom and that α_s(M_Z) = 2/17 is taken from RS. No downstream theorems are listed, so the result functions as a direct numerical bridge between the general beta0 definition and the running statements that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.