DispersionMinCert
plain-language theorem explainer
A certificate bundle packing an optimal RG scale μ_opt together with certified lower and upper bounds that sandwich it. Anyone auditing the non-circularity of the anchor scale μ⋆ ≈ 182.201 GeV cites this as the data shape for the external dispersion-minimum claim. It is a plain structure definition: three reals plus two ordering proofs, no computation inside.
Claim. A dispersion-minimum certificate is a triple of real numbers $(\mu_{\mathrm{opt}},\mu_{\mathrm{lower}},\mu_{\mathrm{upper}})$ such that $\mu_{\mathrm{lower}}\le\mu_{\mathrm{upper}}$ and $\mu_{\mathrm{lower}}\le\mu_{\mathrm{opt}}\le\mu_{\mathrm{upper}}$. The intended reading is that the variance of the anomalous-dimension vector $\mathrm{Var}(\gamma)$ is minimized at $\mu_{\mathrm{opt}}$, with the optimum certified to lie in $[\mu_{\mathrm{lower}},\mu_{\mathrm{upper}}]$.
background
The module certifies that the RS anchor scale $\mu^\star=182.201,\mathrm{GeV}$ is fixed by PMS/BLM stationarity of the SM RG flow, not by measured fermion masses. Lean proves the structural half (stationarity when $\gamma_m(\mu^\star)=0$, mass-independence of the SM beta functions, $\lambda=\ln\varphi$, and positivity). The numerical half (that $\gamma_m$ vanishes near $182.201$ and that this scale uniquely minimizes dispersion) is imported as certified data.
Dispersion here is the spread of the anomalous-dimension vector across species; minimizing $\mathrm{Var}(\gamma)$ is the PMS optimality criterion used to pick $\mu^\star$. Related scale and dispersion primitives appear elsewhere in the monolith (phi-ladder scales, lattice-Laplacian dispersion), but this structure only packages the certified numerical window around the optimum.
The honesty principle of the module is that Lean owns structure while external numerics own the concrete value and uniqueness claim; this certificate is the typed boundary for the latter.
proof idea
No proof body: this is a structure definition. Fields are three reals (mu_opt, mu_lower, mu_upper) and two Prop fields enforcing $\mu_{\mathrm{lower}}\le\mu_{\mathrm{upper}}$ and membership of the optimum in that interval. Inhabitants discharge the inequalities by norm_num (see the sibling certified_dispersion_minimum).
why it matters
Fills certified claim C2 of the module: uniqueness of $\mu^\star$ as the dispersion-minimizing scale, with the concrete window $[180,185]$ and optimum $182.201$. The sibling certified_dispersion_minimum is the canonical inhabitant; NonCircularityCert consumes a DispersionMinCert as one arm of the full non-circularity bundle (alongside proven stationarity, mass-independent betas, and positivity).
Without this shape, the external PMS optimization result would sit outside the typed certificate surface. It does not itself invoke the forcing chain (T0–T8) or the RCL; it only anchors the numerical scale that later RS mass and coupling ladders treat as $\mu^\star$. The open boundary remains that uniqueness and the exact $182.201$ value are certified, not derived inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.