cert
plain-language theorem explainer
Packages three structural facts about the Standard Model domain cost into one certificate: cost vanishes when mass equals energy scale, cost is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing RS structural module 10 (electron-mass calibration, parameter-free SM predictions) uses this bundle. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate recording that (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; and (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 SM predictions are parameter-free. The local cost on mass/energy pairs is the domain cost: a real-valued function built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (the unique cost forced by the Recognition Composition Law).
The certificate structure demands three elementary properties of that cost and of a fixed positive threshold used for structural comparisons: diagonal vanishing (equal arguments cost nothing), nonnegativity on the positive quadrant, and positivity of the threshold. Upstream, the foundation lemma that every recognition-event cost is nonnegative (via $J\ge 0$) supplies the same sign convention used here for domain cost.
proof idea
One-line structure construction. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further rewriting or case analysis occurs.
why it matters
Gives a single inhabited certificate object for RS Standard Model structural module 10, so downstream SM structural theorems can assume diagonal vanishing, cost nonnegativity, and a positive threshold without re-proving them. Fits the module claim of a structural theorem with zero sorry and zero axioms after $E_{\mathrm{coh}}$ is fixed by the electron mass. No used-by edges are recorded yet; the natural consumer is any lemma that needs the bundled certificate rather than the three facts separately. Ties to the J-uniqueness landmark (T5) only through the shared nonnegativity of recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.