cert
plain-language theorem explainer
Packages three structural facts about the Materials-domain cost at recognition rung 43 into one certificate record: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Materials or RS-certificate consumers cite it as the inhabited witness that the domain cost is a well-formed J-style cost. The body is a pure structure assembly of three sibling lemmas.
Claim. There is a Materials rung-43 structural certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Materials domain at recognition rung 43 (Plan v7, 120th pass), with status structural theorem: zero sorry, zero axiom. The domain cost is the local cost functional on mass/energy pairs; the certificate structure requires it to vanish on the equal-argument diagonal, stay nonnegative on the positive orthant, and sit under a positive canonical threshold.
Upstream, the foundation cost law already guarantees nonnegativity of recognition-event cost via the J-cost: "The cost of any recognition event is non-negative," proved from Jcost_nonneg at positive state. Here the Materials module specializes that pattern to a two-argument domain cost and packages the three structural obligations into StructMaterialsM43Cert.
proof idea
One-line structure assembly, not a derivation. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further tactics or algebraic work appear in the body.
why it matters
Gives the inhabited Materials rung-43 structural certificate that the module advertises as a structural RS prediction. Downstream the sibling cert_inhabited and any Materials consumers that demand a StructMaterialsM43Cert witness can point at this record rather than re-proving the three obligations. It sits in the materials branch of the RS certificate stack: domain cost shaped like the foundation J-cost (nonnegative, zero on the identity diagonal), with a positive threshold ready for comparison against rung-scale predictions. No open sorry remains in this module; the declaration closes the packaging step for the three already-proved structural facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.