beta0
plain-language theorem explainer
The one-loop beta function coefficient b₀(N_f) equals (11 N_c - 2 N_f)/(12 π) with N_c fixed at three colors. QCD researchers evolving the strong coupling from the Z-pole downward cite this expression inside the Recognition Science renormalization group. It is supplied as a direct arithmetic definition that encodes the standard SU(3) one-loop result.
Claim. $b_0(N_f) = (11 N_c - 2 N_f)/(12 π)$ where $N_c = 3$ is the number of colors.
background
The module initializes α_s at the Z boson mass and evolves it to nuclear scales via the one-loop renormalization group. It fixes N_c = 3 and introduces b₀ as the coefficient that multiplies the logarithmic term. The same N_c appears upstream in the two-loop extension, where it also defines the fundamental Casimir C_F = 4/3.
proof idea
Direct definition. The body is the arithmetic expression (11 * (N_c : ℝ) - 2 * (N_f : ℝ)) / (12 * Real.pi) with N_c substituted from its sibling definition.
why it matters
b₀ feeds the running formula alpha_s_running, the positivity theorem asymptotic_freedom, and the evaluation beta0_at_Z. It is re-exported as beta0QCDReal in the RGTransport layer. Within the Recognition Science framework it supplies the concrete one-loop kernel required once the gauge group is fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.