cert
plain-language theorem explainer
Packages three structural facts about the materials domain cost into one certificate: the cost vanishes when measured against itself, stays nonnegative for positive arguments, and the canonical threshold is strictly positive. Materials and calibration proofs cite this object as the single witness that module 10 is fully discharged. Construction is a pure structure assembly from three sibling lemmas.
Claim. There is a materials structural certificate whose fields assert: (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 sits in the Recognition Science materials layer. After the coherence energy $E_{\mathrm{coh}}$ is fixed once from the electron mass, every materials prediction is required to be parameter-free. The local cost on a materials domain is a real-valued function of two positive scales (mass-like and energy-like arguments). It is built from the global J-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative and vanishes only at the identity $x=1$.
The certificate structure collects exactly three obligations: diagonal vanishing (self-comparison costs nothing), nonnegativity on the positive orthant, and positivity of a fixed numerical threshold used later as a decision cut. Upstream, the foundation lemma that every recognition-event cost is nonnegative (via $J\ge 0$) supplies the pattern that the materials nonnegativity lemma mirrors.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site.
why it matters
Gives the single inhabited certificate that marks RS materials structural module 10 as closed: zero sorry, zero axiom, and fully parameter-free once $E_{\mathrm{coh}}$ is set by the electron mass. Downstream consumers (none yet wired in the graph) can take this object as proof that the domain cost is a genuine cost functional with a usable positive threshold. In the broader forcing chain it sits downstream of J-uniqueness (T5) and the nonnegativity of recognition cost, and upstream of any materials prediction that needs a certified cut. It does not itself compute a mass or a coupling; it only certifies the structural scaffolding those predictions rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.