canonical_anchor_cert
plain-language theorem explainer
Packages the anchor scale μ⋆ = 182.201 GeV as a complete non-circularity certificate: positivity, mass-independent SM beta structure, and externally certified stationarity and dispersion bounds. Anyone citing the RS claim that the anchor is fixed without fermion-mass inputs uses this witness. Construction is a structure instance wiring proven structural lemmas to certified numeric certificates, with scale-match by reflexivity.
Claim. The canonical non-circularity certificate is the package with scale $\mu^\star$, a proof that $\mu^\star > 0$, the canonical Standard Model beta-function structure (mass-independent by group representation data), certified stationarity bounds at $\mu^\star$, certified dispersion-minimum data, and definitional scale-matching equalities.
background
This module certifies that the RS anchor scale $\mu^\star = 182.201,\mathrm{GeV}$ is fixed by structural RG properties rather than by measured fermion masses. Non-circularity means: (i) $\mu^\star$ solves a stationarity condition on the RG flow (PMS/BLM style), (ii) that condition uses only SM gauge-group beta data, and (iii) no Yukawa or fermion-mass inputs enter the determination.
NonCircularityCert separates what Lean proves from what is certified externally. Proven pieces are positivity of the scale, mass-independence of the SM beta structure, the $\phi$-forced normalization $\lambda = \ln\phi$, and the structural stationarity implication. Certified pieces are the numerical vanishing of anomalous dimensions at $\mu^\star$, uniqueness as a dispersion minimum, and the concrete GeV value from PMS optimization.
Sibling facts wired in include the canonical SM beta package, positivity of $\mu^\star$, certified stationarity bounds, and the certified dispersion minimum. The honesty principle of the module is that structure is proved in Lean while numerics remain external certificates.
proof idea
Definitional structure instance, not a tactic proof. Fields are filled as: scale $\leftarrow \mu^\star$; positivity $\leftarrow$ the existing positivity lemma for $\mu^\star$; beta structure $\leftarrow$ the canonical SM beta package; stationarity $\leftarrow$ certified stationarity bounds; dispersion $\leftarrow$ certified dispersion minimum. The scale-match field is discharged by constructor followed by reflexivity on both sides. No algebraic rewriting beyond that wiring.
why it matters
This is the single witness object for the module's main claims. Downstream, mass-independence of the canonical anchor is immediate from the beta-structure field; parameter-freeness combines that with the certified bounds; the value theorem reads $\mu = 182.201$ off the package; and the main certificate theorem exhibits a non-circularity certificate with that scale, mass-independence, and parameter-free status.
In the RS verification layer this closes the non-circularity gap for the mass-ladder yardstick: the anchor used by the $\phi$-ladder mass formula must not smuggle fermion masses back into the scale choice. The module is explicit that Lean owns the structural half (P1–P4) while C1–C3 remain external numeric certificates. No forcing-chain step (T5–T8) is re-proved here; the contribution is auditability of the anchor policy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.