beta_is_mass_independent
plain-language theorem explainer
The one-loop QCD coefficient in the canonical SM beta structure equals 11 − 2 n_f/3 for every flavor count n_f, with no mass parameters in the formula. Cited by anyone auditing that anchor-scale stationarity uses only gauge-group data. Proof is definitional: introduce n_f and close by reflexivity against the structure's field.
Claim. For every natural number $n_f$, the one-loop QCD beta coefficient of the canonical Standard Model beta structure satisfies $\beta_0^{\mathrm{QCD}}(n_f) = 11 - \frac{2 n_f}{3}$ (as a rational identity).
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, without feeding measured fermion masses into the choice of scale. Non-circularity, as stated in the module doc, requires three ingredients: a stationarity condition, beta functions built only from SM group structure, and no mass inputs in the determination of $\mu_\star$.
THEOREM P2 isolates the second ingredient. In ordinary QCD the one-loop coefficient is the representation-theoretic count $\beta_0 = 11 - 2 n_f/3$, where $n_f$ is the number of active Dirac flavors. That formula depends on the adjoint and fundamental Casimirs of $SU(3)$, not on Yukawa couplings or pole masses. The canonical SM beta structure packages this standard coefficient as a field; the present result records that the field is exactly the mass-free formula.
Sibling material in the same certificate covers stationarity structure (P1), the $\lambda = \ln\varphi$ normalization (P3), and positivity of $\mu_\star$ (P4). External numerics (C1–C3) remain outside Lean.
proof idea
Term-mode, two steps. Introduce the free natural $n_f$, then close with rfl. The goal is definitional equality between the projected field canonicalSMBeta.beta0_QCD nf and the rational expression $(11 : \mathbb{Q}) - (2 : \mathbb{Q})\cdot n_f/3$, so no rewriting or external lemmas are required. The mass-independence claim is therefore the observation that the defining body contains only the discrete flavor count, not continuous mass parameters.
why it matters
This is the Lean discharge of THEOREM P2 in the Anchor Scale Non-Circularity Certificate: SM beta coefficients depend only on gauge-group representations. Together with P1 (stationarity when mass anomalous dimensions vanish), P3 ($\lambda = \ln\varphi$ forced by the cost), and P4 ($\mu_\star > 0$), it underwrites the structural half of the honesty split in the module: Lean proves the mass-free architecture; external tools certify the numerical root and uniqueness.
In the broader RS picture the anchor $\mu_\star$ sets the rung reference for the $\varphi$-ladder mass formula. If beta functions smuggled fermion masses, the ladder would be circular. P2 blocks that loop at the coefficient level. Downstream certificate aggregators (NonCircularityCert, is_mass_independent, stationarity bounds) are the intended consumers, even though the dependency graph currently lists no used_by edges for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.