b0
plain-language theorem explainer
b0 supplies the one-loop beta coefficient beta0(N_f) = (11*3 - 2*N_f)/(12*pi) for QCD running with N_c fixed at three. Mass anomalous dimension calculations and two-loop alpha_s formulas in the Recognition Science framework cite this to set the leading term in the beta function. The declaration is a direct arithmetic definition with no additional lemmas.
Claim. The one-loop coefficient in the QCD beta function is $b_0(N_f) = (11 N_c - 2 N_f)/(12 pi)$ where $N_c = 3$.
background
The module implements the two-loop running of alpha_s in the MS-bar scheme. The beta function takes the form d alpha_s / d log mu^2 = -beta0 alpha_s^2 - beta1 alpha_s^3, with beta0 defined here for variable active flavors N_f. The sibling N_c declaration fixes the number of colors at 3, matching the canonical SU(3) expression quoted in the module documentation: 'beta0 = (11 N_c - 2 N_f) / (12 pi)'. Upstream canonical arithmetic objects supply the underlying real-number operations but are not invoked inside the body.
proof idea
The declaration is a one-line definition that directly encodes the standard expression (11 * N_c - 2 * N_f) / (12 * Real.pi) with N_c cast to real.
why it matters
This definition anchors the two-loop running formula alpha_s_two_loop and the mass running ratios mass_ratio_leading and mass_ratio_two_loop. It implements the beta0 term in the module's two-loop beta function, connecting to the Recognition Science constants via the phi-ladder in related physics modules. It closes the one-loop limit case in alpha_s_two_loop_b1_zero_eq_one_loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.