cert
plain-language theorem explainer
Packages three structural facts for Materials Module 4 (Mohs diamond / φ⁵) into a single certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Materials or RS-constants workers cite it as the inhabited witness that the module's cost interface is well-formed. Proof is a pure structure assembly of 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
Materials RS Module 4 is a structural (zero-sorry) fragment tying the Mohs hardness of diamond to the RS constant $\varphi^5 \approx 11.09$, read as order-10 on the Mohs scale. The local cost interface is a two-argument real function domainCost, meant as the materials-domain specialization of the recognition J-cost.
The certificate structure demands three interface laws: diagonal vanishing (equal measure and expectation cost nothing), nonnegativity for positive arguments, and positivity of a fixed canonicalThreshold. Upstream, the foundation lemma cost_nonneg states that "the cost of any recognition event is non-negative," via nonnegativity of $J$; the materials nonnegativity field is the corresponding domain-level fact.
Notation is ordinary reals; no units conversion is performed inside the certificate itself.
proof idea
One-line structure construction. The three fields of RSMatl004Cert are filled by the already-proved sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is done at this site; it is pure packaging.
why it matters
Gives the inhabited structural certificate for Module 4, so downstream materials arguments can assume a single well-formed cost interface rather than three separate lemmas. Aligns with the RS landmark $Z_{\mathrm{cf}} = \varphi^5 \in (11,12)$ and the primer constant band around $\varphi^5$, here read against Mohs 10 (diamond). Status is STRUCTURAL THEOREM per the module doc. No used_by edges are recorded yet; the immediate consumer in-module is the inhabitedness witness for the same certificate type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.