certified_stationarity_bounds
plain-language theorem explainer
Packages the external SM RG numerics that place the PMS/BLM stationarity scale at μ⋆ = 182.201 GeV with sub-permille tolerance ε = 0.001. Anyone arguing that the RS mass anchor is non-circular cites this certificate as the numerical half of the claim. Construction is a structure instance: literal bounds plus positivity discharged by norm_num.
Claim. The certified stationarity record fixes the scale $\mu_\star = 182.201$ (GeV) and tolerance $\varepsilon = 0.001$, and asserts the positivity facts $0 < \mu_\star$ and $0 < \varepsilon$. Intended reading: $|\gamma(\mu_\star)| < \varepsilon$ for all species, as certified from external SM RG runs.
background
The module certifies that the RS anchor scale $\mu_\star = 182.201$ GeV is fixed by PMS/BLM stationarity of the SM RG flow, not by measured fermion masses. Lean proves the structural half (stationarity implication, mass-independence of $\beta_s,\beta_e$, $\lambda = \ln\varphi$, positivity). External tools (RunDec-class SM RG) supply the numerical half: that anomalous dimensions vanish near this scale.
StationarityCert is the bundle for that numerical half: a scale $\mu$, a tolerance $\varepsilon$, and proofs that both are positive. The doc-comment states the intended content as $|\gamma(\mu_\star)| < \varepsilon$ for all species. Downstream, this record is plugged into the canonical non-circularity certificate alongside a dispersion-minimum certificate and the structural SM beta data.
proof idea
Definitional structure instance, not a derived theorem. Sets mu to the literal 182.201 and epsilon to 0.001 (sub-permille). Both positivity fields are closed by norm_num on those decimals. No upstream lemmas about projectors, path-sum measures, or lattice dispersion are invoked; those name-collisions on mu/A are unrelated identifiers elsewhere in the monolith.
why it matters
This is the C1 numerical slot in the module's honesty split: Lean owns structure (P1–P4); external RG owns the concrete stationarity check. It is wired directly into canonical_anchor_cert as the stationarity_cert field, and anchor_parameter_free unfolds it and re-checks positivity by norm_num when proving the canonical anchor is parameter-free.
In the broader RS picture the anchor feeds the mass ladder (yardstick times $\varphi$ raised to rung offsets). Non-circularity of $\mu_\star$ is what keeps that ladder from smuggling fermion masses into the scale that normalizes them. The value itself is not forced by the T0–T8 chain; it is an SM-side PMS optimum certified here for use by the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.