anchor_scale_certified
plain-language theorem explainer
There exists a non-circularity certificate for the RG anchor scale μ⋆ = 182.201 GeV that is mass-independent and parameter-free. Anyone citing the RS claim that the mass ladder is not fit to fermion masses needs this existence result. The proof packages a canonical certificate with three structural lemmas; numerical stationarity bounds remain externally certified, so the claim is still scaffolding.
Claim. There exists a non-circularity certificate $C$ for the SM RG flow such that the certified scale equals $\mu_\star = 182.201\,\mathrm{GeV}$, $C$ is mass-independent (its beta structure depends only on gauge representations, not Yukawas), and $C$ is parameter-free (stationarity and dispersion bounds hold with no free fit parameters).
background
The module certifies that the RS anchor scale $\mu_\star = 182.201,\mathrm{GeV}$ is fixed by PMS/BLM-style stationarity of the SM renormalization-group flow, not by fitting fermion masses. Non-circularity means: (i) $\mu_\star$ solves a stationarity condition on the anomalous dimensions, (ii) that condition uses only SM group structure (beta functions), and (iii) no measured fermion masses enter the determination.
A NonCircularityCert packages the scale $\mu$, a positivity proof, an SM beta structure, plus externally certified stationarity and dispersion-minimum data. Sibling facts already separate structure from numerics: stationarity is equivalent to $\gamma(\mu_\star)=0$; SM betas are mass-independent by formula inspection; $\lambda=\ln\varphi$ is forced by the cost function; and $\mu_\star>0$ is pure arithmetic.
The honesty boundary is explicit: Lean owns the structural non-circularity claim; the concrete number 182.201 and the bounds $|\gamma(182.201)|<0.001$ are trusted from external SM RG tools (analogous to RunDec), not derived inside the kernel.
proof idea
One-line existence proof: introduce the canonical anchor certificate and discharge the three conjuncts by the named structural lemmas for the anchor value, mass-independence, and parameter-free status. No new algebra is done here; the work is packaging. The surrounding module comments list which pieces are fully proved in Lean versus which numerical bounds remain external certificates feeding the structure fields.
why it matters
In Recognition Science the mass formula sits on a $\varphi$-ladder with a fixed yardstick; if that yardstick were tuned to fermion masses, the ladder would be circular. This theorem is the main certificate that $\mu_\star$ is instead fixed by RG stationarity and SM group structure alone, with $\lambda=\ln\varphi$ forced by the cost side (linking to the T5/T6 J-uniqueness and golden fixed-point chain).
No downstream consumers are wired yet (used_by is empty), so the declaration currently closes the verification module rather than feeding a larger theorem. It is the honest boundary object: structure proved, numerics certified externally. Closing the remaining scaffold means replacing external stationarity/dispersion certificates with fully internal proofs or with machine-checked bounds at the stated tolerance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.