RSMatl004Cert
plain-language theorem explainer
Certificate bundle for Materials Module 4 (diamond / Mohs 10): three structural props on the materials domain cost and the canonical threshold. Anyone citing the module's inhabited certificate or the packed `cert` value depends on this shape. Pure structure definition; the three fields are Prop obligations discharged elsewhere by sibling lemmas.
Claim. A materials certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$; (ii) for all positive $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Materials RS Module 4 is the structural (zero-sorry) treatment of diamond on the Mohs scale: $\varphi^5\approx 11.09$ is identified with Mohs hardness 10. The module works in RS-native units and imports the global cost layer and constants.
Domain cost is the materials-side specialization of recognition cost on a pair of positive reals (mass-like and energy-like arguments). The canonical threshold is the positive scale against which that cost is compared in this module. Upstream, the foundation result cost_nonneg states that every recognition event has nonnegative cost, via nonnegativity of the J-cost on positive states.
The three fields of this structure are exactly the local obligations needed to treat the diamond / Mohs identification as a certified structural fact rather than an informal numerology claim.
proof idea
No proof body: this is a structure definition whose fields are propositions. Inhabitation is supplied downstream by packing three sibling lemmas (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos) into a single value of this type. The nonnegativity field is the materials-domain analogue of the foundation theorem that recognition-event cost is nonnegative.
why it matters
Gives the typed interface for Module 4's structural certificate. Downstream, cert assembles the three sibling proofs into one value of this type, and cert_inhabited records Nonempty of the certificate, closing the module as a zero-sorry structural theorem.
In the broader RS picture this sits next to the $\varphi$-ladder and the creation / coincidence band: the primer's $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$ is the same scale the module reads as Mohs 10 for diamond. The certificate does not derive Mohs hardness from first principles; it packages the cost and threshold facts the module needs so that identification can be cited as a certified structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.