NonCircularityCert
plain-language theorem explainer
Bundles the full non-circularity certificate for an RG anchor scale μ: positivity, SM beta structure (group factors only), external stationarity and dispersion-minimum certificates, and a scale-match constraint. Anyone arguing that μ⋆ is fixed without fermion-mass inputs cites this record type. It is a pure data structure; no proof body.
Claim. A non-circularity certificate is a record consisting of a scale $\mu\in\mathbb{R}$ with $\mu>0$, an SM beta-function structure (QCD/QED $\beta_0$ coefficients depending only on gauge representations), a stationarity certificate (external bound $|\gamma(\mu)|<\varepsilon$), a dispersion-minimum certificate (external uniqueness of the variance-minimizing scale), and the requirement that both external certificates are issued at the same target $\mu$.
background
The module certifies that the RS anchor scale $\mu_\star=182.201,\mathrm{GeV}$ is fixed by PMS/BLM stationarity on the SM RG flow, not by measured fermion masses. Lean proves structural facts (stationarity implication, mass-independence of $\beta$ coefficients, $\lambda=\ln\varphi$ normalization, positivity). External numerics certify $\gamma_m(\mu_\star)\approx 0$, uniqueness of the dispersion minimum, and the concrete GeV value.
SMBetaStructure packages $\beta_0^{\mathrm{QCD}}(n_f)$ and $\beta_0^{\mathrm{QED}}$ as functions of active flavor count only, with asymptotic freedom for $n_f\le 16$. StationarityCert holds a scale, a positive tolerance $\varepsilon$, and (externally) $|\gamma|<\varepsilon$. DispersionMinCert holds an optimal scale inside certified bounds. The present record glues those pieces and forces scale agreement.
proof idea
No proof: this is a structure definition. Fields are the scale $\mu$, the positivity witness, the SM beta structure, the two external certificates, and the propositional equality that both certificates target the same $\mu$. Downstream constructors (e.g. the canonical anchor certificate) fill the fields with muStar, canonicalSMBeta, and the certified stationarity/dispersion bundles.
why it matters
This is the carrier type for the module's honesty split between Lean-proved structure and externally certified numerics. The main theorem anchor_scale_certified asserts existence of such a certificate at $\mu=182.201$ that is mass-independent and parameter-free. The canonical inhabitant canonical_anchor_cert and the predicates is_mass_independent / is_parameter_free are typed against it.
In the RS framework the anchor scale sets the mass-ladder yardstick; non-circularity means that yardstick is not tuned to the fermion masses it later predicts. The certificate formalizes that claim without overstating what Lean alone proves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.