SMBetaStructure
plain-language theorem explainer
Packages the one-loop SM beta coefficients as pure gauge-group data: maps from active flavor count to rational β₀ for QCD and QED, plus the asymptotic-freedom inequality for n_f ≤ 16. Cited by the anchor non-circularity certificate to separate group-structure inputs from mass-dependent Yukawas. Definitional structure only; no proof body.
Claim. A Standard Model beta structure consists of rational one-loop coefficients $\beta_0^{\mathrm{QCD}}(n_f)$ and $\beta_0^{\mathrm{QED}}(n_f)$ as functions of the number of active flavors, together with the requirement that $\beta_0^{\mathrm{QCD}}(n_f) > 0$ whenever $n_f \le 16$ (asymptotic freedom). These coefficients are intended to encode only gauge-group representation data, not fermion masses.
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 and does not feed measured fermion masses back into its own definition. Lean proves the structural half (stationarity shape, mass-independence of betas, $\lambda = \ln\varphi$, positivity of $\mu_\star$); numerics that $\gamma_m(\mu_\star)\approx 0$ and uniqueness of the dispersion minimum are certified externally.
In that setting, the one-loop QCD coefficient is the standard Casimir combination $\beta_0 = (11/3)C_A - (4/3)n_f T_F$ with $C_A = N_c = 3$ and $T_F = 1/2$, while QED uses $\beta_0 = -(4/3)\sum_i Q_i^2$. Both depend only on active representations. The structure records those maps as $\mathbb{N}\to\mathbb{Q}$ plus the positivity bound that encodes asymptotic freedom for $n_f\le 16$.
Sibling material in the same file then instantiates the canonical coefficients and folds the structure into the full non-circularity certificate as the mass-independent beta slot.
proof idea
No proof: this is a structure declaration. It introduces three fields (two coefficient maps and one positivity axiom) and stops. Inhabitants are supplied later by the canonical instance, which plugs in the explicit rational formulas and discharges asymptotic freedom by a short arithmetic argument on $n_f\le 16$.
why it matters
This is the typed carrier for claim P2 of the anchor non-circularity certificate: SM beta functions depend only on gauge representations, not on Yukawa/mass inputs. Downstream, canonicalSMBeta fills the fields with the textbook coefficients, and NonCircularityCert requires an SMBetaStructure field as the proven mass-independent beta package alongside positivity of $\mu$ and the stationarity/dispersion certificates.
Without a structure that isolates group data from masses, the non-circularity claim (anchor fixed by RG stationarity alone) cannot be stated cleanly. In the broader RS picture it supports the honesty split between Lean-proved structure and externally certified numerics for $\mu_\star$, rather than a forcing-chain landmark (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.