cert
plain-language theorem explainer
Packages three structural facts about domain cost and the canonical threshold into one certificate record. Anyone citing the RS structural calibration layer (E_coh fixed once by the electron mass, predictions parameter-free) would point here. The definition is a pure field-wiring of three already-proved sibling lemmas into the certificate structure.
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
Module 10 of the RS foundation structural series fixes the coherence energy $E_{\mathrm{coh}}$ once from the electron mass and then treats all further predictions as parameter-free. Status is structural: zero sorry, zero axioms.
The certificate structure collects three elementary properties of a real-valued domain cost on pairs of positive scales: vanishing on the diagonal (equal arguments), nonnegativity off the diagonal, and positivity of a fixed canonical threshold used as a comparison scale. Upstream, the ObserverForcing development already records that every recognition-event cost is nonnegative via the J-cost minimum at identity ($x=1$), which is the same nonnegativity pattern reused here for domain cost.
proof idea
Pure structure construction. Each of the three certificate fields is filled by the corresponding in-module lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Gives a single named inhabitant of the structural certificate for module 10, so downstream calibration or forcing arguments can assume the three cost/threshold facts as one package rather than three separate hypotheses. Fits the RS forcing chain's cost layer (J-cost uniqueness and nonnegativity) and the module's claim that once $E_{\mathrm{coh}}$ is set by the electron mass, the remaining structural inequalities are theorem-level. No used_by edges are recorded yet; the immediate sibling cert_inhabited is the natural consumer that witnesses nonemptiness of the certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.