cert
plain-language theorem explainer
Certificate packing three structural facts for the iron-melting materials module: domain cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the phi-ladder iron melt match (1814 K vs 1811 K) uses this bundle. It is a structure instance that wires three local lemmas; no new mathematics.
Claim. There is a certificate asserting: (i) the materials domain cost satisfies $\mathrm{cost}(r,r)=0$ for every nonzero real $r$; (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 5 of the RS materials layer treats iron melting as a phi-ladder prediction: $\phi^{15}\cdot\phi^{0.7},\mathrm{K}=1814,\mathrm{K}$ against the experimental $1811,\mathrm{K}$ (0.2% relative error). The module is marked structural (zero sorry, zero axiom).
The local cost is a two-argument real function domainCost, intended as the materials-side specialization of the Recognition J-cost. The structure RSMatl005Cert packages the three elementary properties any such cost must satisfy before thresholds or melt criteria are applied: diagonal vanishing, nonnegativity on the positive quadrant, and a positive canonical threshold.
Upstream, the foundation lemma cost_nonneg already records that every recognition event has nonnegative J-cost (0 \le e.cost), via Jcost_nonneg at positive state. The materials certificate reuses that nonnegativity pattern at the domain-cost level.
proof idea
One-line structure instance. The three fields of RSMatl005Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No tactic proof and no new argument; pure wiring of preexisting facts into the certificate record.
why it matters
Gives a single named inhabitant of the materials-module-5 certificate so downstream material claims can assume the cost axioms without re-proving them. The module doc ties the package to the iron melting MATCH on the phi ladder ($\phi^{15}\phi^{0.7}$ K). Within the broader RS chain this sits downstream of J-cost nonnegativity (T5 / ObserverForcing) and upstream of any threshold comparison that would certify a melt temperature. No used_by edges are recorded yet; the companion cert_inhabited is the natural consumer. Does not itself compute or prove the 1814 K figure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.