canonicalSMBeta
plain-language theorem explainer
Canonical one-loop SM beta coefficients: QCD β₀(n_f)=11−2n_f/3 and a simplified QED β₀≡0, packaged with a proof of asymptotic freedom for n_f≤16. Cited by anyone assembling the anchor-scale non-circularity certificate, since stationarity and mass-independence arguments need a concrete β structure. The body is a structure instance; positivity is a short rational inequality.
Claim. The canonical Standard Model beta structure assigns $\beta_0^{\mathrm{QCD}}(n_f)=11-\frac{2n_f}{3}$ and $\beta_0^{\mathrm{QED}}(n_f)=0$ (charge-sum omitted), and asserts $\beta_0^{\mathrm{QCD}}(n_f)>0$ whenever $n_f\le 16$.
background
The module certifies that the RS anchor scale $\mu_\star=182.201,\mathrm{GeV}$ is fixed by PMS/BLM stationarity on the RG flow, using only SM group structure and no measured fermion masses. Lean proves the structural claims (stationarity as vanishing anomalous dimension, mass-independence of $\beta$, $\lambda=\ln\varphi$, positivity of $\mu_\star$); numerics for $\gamma_m(\mu_\star)\approx 0$ and uniqueness are certified externally.
SMBetaStructure packages the one-loop gauge beta coefficients as functions of active flavor count alone. The QCD formula is the standard Casimir reduction $(11/3)C_A-(4/3)n_f T_F$ with $C_A=3$, $T_F=1/2$, which collapses to $11-2n_f/3$. QED is the charge-squared sum; here it is stubbed to zero. The structure also requires asymptotic freedom: $\beta_0^{\mathrm{QCD}}>0$ for $n_f\le 16$.
proof idea
Definitional instance of SMBetaStructure. QCD coefficient is the closed rational formula; QED is the constant zero map. Asymptotic freedom is proved by bounding: if $n_f\le 16$ then $2n_f/3\le 32/3<11$, so $11-2n_f/3>0$, via div_le_div_of_nonneg_right, mul_le_mul_of_nonneg_left, norm_num, and linarith.
why it matters
Supplies the concrete $\beta$ data for theorem P2 (beta_is_mass_independent), which states that the QCD coefficient equals $11-2n_f/3$ with no mass parameters, and for canonical_anchor_cert, the full non-circularity certificate that wires $\mu_\star$, this beta structure, stationarity bounds, and the dispersion minimum. Without a mass-free $\beta$ instance, the claim that $\mu_\star$ is fixed by group structure alone cannot be stated. Fits the module honesty split: structure in Lean, numerics certified outside. No direct T0–T8 forcing step; it is verification infrastructure for the anchor used downstream in RS mass and coupling transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.