cert
plain-language theorem explainer
Packages three structural facts about the RS5 electron-mass domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone needing an inhabited ElectronMassRS5Cert cites this. The body is a structure instance that wires three sibling lemmas.
Claim. There is a certificate asserting: (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
The module treats the RS5 electron-mass claim as a structural theorem: $m_e = E_{\mathrm{coh}},\varphi^3$ recovers $0.511,\mathrm{MeV}$ to about $0.2%$. The certificate type bundles the minimal analytic properties of the domain cost used in that derivation.
Domain cost is the local cost functional on mass/energy pairs; its diagonal vanishing and nonnegativity mirror the global J-cost facts (J vanishes at the identity and is nonnegative). The upstream result cost_nonneg states that every recognition event has nonnegative cost via Jcost_nonneg. The canonical threshold is the positive cutoff against which the electron rung is compared.
This definition does not re-prove those inequalities; it only assembles the in-module lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into one inhabited record.
proof idea
One-line structure instance. Field cost_at_eq is filled by domainCost_at_eq; cost_nonneg by domainCost_nonneg; threshold_pos by canonicalThreshold_pos. No extra tactics or algebraic work.
why it matters
Gives a single named witness that the RS5 electron-mass domain cost satisfies the three structural axioms required by the certificate type. Downstream, cert_inhabited and any consumer of ElectronMassRS5Cert can point at this object rather than re-listing the three lemmas.
In the broader framework this sits under the mass-ladder story: yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, with the electron fixed at the $\varphi^3 E_{\mathrm{coh}}$ rung. The certificate does not itself compute the MeV number; it only locks the cost-side hypotheses that make that identification well-posed. No used-by edges are recorded yet, so its role is local scaffolding for the electron-mass session.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.