RSMatl005Cert
plain-language theorem explainer
Certificate bundle for Materials Module 5 (iron melting): the domain cost vanishes on the diagonal, stays non-negative off it for positive arguments, and the canonical threshold is strictly positive. Materials and RS-constants workers cite it to discharge the structural side conditions of the phi-ladder melt match. It is a pure structure definition; inhabitance is supplied separately by packing three sibling lemmas.
Claim. A certificate for the iron-melting materials module consists of three facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Materials RS Module 5 targets the iron melting point via the phi-ladder: $\phi^{15}\cdot\phi^{0.7},\mathrm{K}\approx 1814,\mathrm{K}$ versus the experimental $1811,\mathrm{K}$ (about $0.2%$ relative error). The module is marked structural: zero sorry, zero axioms.
The domain cost is the materials-side specialization of the Recognition Science J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). On the diagonal it must vanish (perfect match of the two arguments); off-diagonal and for positive mass/energy-like arguments it must stay nonnegative, mirroring the foundation fact that every recognition event has nonnegative cost.
The canonical threshold is the positive cutoff used to gate the melt comparison. Upstream, cost_nonneg in ObserverForcing states that the cost of any recognition event is nonnegative, via nonnegativity of Jcost on positive states.
proof idea
No proof body: this is a structure (record type) with three propositional fields. Inhabitance is not proved here. The sibling definition cert packs domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into one term of this type; cert_inhabited then wraps that term as Nonempty RSMatl005Cert. The mathematical work lives in those three sibling lemmas, not in the structure itself.
why it matters
The structure is the typed interface that Module 5 exposes as its structural theorem package. Downstream, cert is the concrete witness and cert_inhabited records that the certificate type is nonempty, closing the module's "STRUCTURAL THEOREM (0 sorry, 0 axiom)" claim for the iron melt match.
In the broader RS stack this sits under Materials rather than the T0–T8 forcing chain, but it reuses the same J-cost nonnegativity and identity-minimum discipline forced at T5. The numerical claim (phi-ladder temperature within $0.2%$ of iron's melt point) is the scientific payload; this certificate only locks the cost and threshold side conditions so that payload is not floating free of the cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.