RSSTDStructural010Cert
plain-language theorem explainer
Certificate bundling three structural properties for RS Standard Model module 10: diagonal domain cost vanishes off zero, domain cost is nonnegative on positive mass and energy, and the canonical threshold is strictly positive. Cited by anyone assembling the inhabited structural certificate for electron-mass calibration. It is a pure structure definition whose fields are discharged by sibling lemmas.
Claim. A certificate consisting of three facts: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 10 of the RS Standard Model structural layer fixes the coherence energy $E_{\mathrm{coh}}$ once from the electron mass, after which all predictions are parameter-free. The local status claim is a structural theorem with no sorry and no axioms.
Domain cost is the module's real-valued cost on mass/energy pairs; the diagonal identity domainCost r r = 0 (for $r \neq 0$) is the fixed-point minimum of that cost. Nonnegativity of domain cost on the positive quadrant mirrors the foundation fact that every recognition event has nonnegative cost, proved upstream via nonnegativity of the J-cost on positive states.
The canonical threshold is the positive cutoff used to gate structural comparisons in this calibration layer. The three fields of the certificate are exactly the Prop-valued obligations that a concrete witness must supply.
proof idea
No proof body: this is a structure declaration. The three fields are named hypotheses (Propositions) that any inhabitant must provide. Downstream, cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that witness as Nonempty.
why it matters
Gives the typed interface for the module-10 structural certificate. Downstream cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural theorem for this layer.
In the broader RS program this sits under Standard Model calibration: once $E_{\mathrm{coh}}$ is fixed by the electron mass, structural cost identities and a positive threshold underwrite parameter-free predictions. It inherits the foundation nonnegativity of recognition cost (J-cost minimum at the identity) without reopening the forcing chain T0–T8. No open scaffold remains in this module; the certificate is fully discharged by the sibling lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.