certified_dispersion_minimum
plain-language theorem explainer
Packages the certified claim that RG dispersion of mass anomalous dimensions is minimized at 182.201 GeV, inside the interval [180,185]. Downstream non-circularity and parameter-free anchor certificates cite it as the external numerical half of the anchor-scale story. The Lean body only checks bound ordering and membership by norm_num; the optimality value itself is imported certification, not a derived theorem.
Claim. There is a certified dispersion-minimum record with optimal scale $\mu_{\mathrm{opt}}=182.201$, lower bound $180$, and upper bound $185$, such that $180\le 185$ and $180\le 182.201\le 185$. The record asserts that the variance of the mass anomalous dimensions $\mathrm{Var}(\gamma)$ is minimized at this scale.
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, without feeding measured fermion masses into the choice of scale. Non-circularity splits into Lean-proved structure (stationarity when $\gamma_m(\mu^\star)=0$, mass-independence of gauge betas, $\lambda=\ln\varphi$, positivity) and externally certified numerics (vanishing of $\gamma_m$, uniqueness of the dispersion minimum, the concrete GeV value).
DispersionMinCert is the certified half for dispersion: it records an optimal scale together with a closed interval that is supposed to contain the unique minimizer of $\mathrm{Var}(\gamma)$. The present definition is the concrete inhabitant used by the canonical anchor certificate. Related siblings handle stationarity bounds and the SM beta structure; together they feed the full non-circularity certificate.
proof idea
Structure instance, not a derived existence proof. Fields are set to $\mu_{\mathrm{opt}}=182.201$, $\mu_{\mathrm{lower}}=180$, $\mu_{\mathrm{upper}}=185$. The two proof obligations (bounds_ordered and mu_in_range) are discharged by norm_num (with constructor to split the conjunction). No RG lemma is invoked; the optimality claim is trusted external input packaged for downstream certificates.
why it matters
Fills certified items C2/C3 in the module honesty split: uniqueness of $\mu^\star$ as dispersion minimizer and the concrete PMS value 182.201 GeV. canonical_anchor_cert plugs this record in as dispersion_cert beside the stationarity certificate and the canonical SM beta structure. The theorem anchor_parameter_free then unfolds the canonical certificate and uses this definition (via simp) to discharge the dispersion half of parameter-freeness.
In the broader RS picture the anchor sits above the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and supplies the mass-ladder yardstick scale without circular mass inputs. The declaration does not close the open ledger-floor bridge; it only seals the numerical dispersion slot so the non-circularity claim can be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.