RSMTHStructural010Cert
plain-language theorem explainer
Certificate structure bundling three calibration facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites the inhabited instance when a single witness of these structural properties is required. Pure definitional packing; proofs live in the field constructors.
Claim. A structural certificate asserts three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_010 is a structural calibration unit: once the coherence energy $E_{\mathrm{coh}}$ is fixed by the electron mass, remaining predictions are parameter-free. The certificate packages the elementary positivity and normalization facts that any such calibration must satisfy.
Domain cost is the real-valued cost assigned to a measured-versus-expected pair $(m,e)$. Its diagonal vanishing says a perfect match carries zero cost; nonnegativity for positive arguments is the quantitative lower bound. Both sit downstream of the Recognition cost calculus, where the J-cost $J(x)=(x+x^{-1})/2-1$ is nonnegative and minimized at the identity $x=1$. Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J$-cost nonnegativity.
The canonical threshold is the positive cutoff used to separate negligible from reportable cost in this structural layer.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is supplied separately by the noncomputable definition cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The companion theorem cert_inhabited then wraps that definition as Nonempty.
why it matters
Gives a single named witness type for the three structural inequalities that underwrite parameter-free RS calibration in this module. Downstream, cert builds an explicit inhabitant and cert_inhabited exposes nonemptiness, so later mathematics modules can assume the package without re-proving diagonal vanishing, cost nonnegativity, or threshold positivity.
In the broader framework this sits under the cost layer forced by T5 (J-uniqueness) and the Recognition Composition Law: nonnegativity and the zero-at-identity minimum are the quantitative backbone of recognition events. The module status line (0 sorry, 0 axiom) marks the package as closed structural content rather than scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.