cert
plain-language theorem explainer
Packages three elementary facts about the materials-domain cost into a single certificate for the copper Debye-temperature module. Anyone citing the structural claim that φ^{12} K ≈ 343 K (6% off experiment) can point here for the supporting cost axioms. The definition is a pure structure inhabitant: it wires three already-proved lemmas into the certificate fields.
Claim. There exists a materials certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Materials RS Module 2 is a structural (zero-sorry) package around the copper Debye temperature. Recognition Science predicts $\phi^{12},\mathrm{K}\approx 321.9,\mathrm{K}$ against the experimental $343,\mathrm{K}$ (about 6% relative error). The module does not derive the Debye formula from first principles; it certifies the cost infrastructure used by that comparison.
The domain cost is the materials-side specialization of the Recognition J-cost $J(x)=(x+x^{-1})/2-1$. Upstream, cost_nonneg in ObserverForcing records that every recognition event has nonnegative cost, via $J\ge 0$ for positive states. The local certificate structure RSMatl002Cert asks three concrete properties of that domain cost and of a positive canonical threshold against which material scales are compared.
proof idea
One-line structure inhabitant. The three fields of RSMatl002Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new algebra is performed; the definition only assembles those three results.
why it matters
Gives a single named witness that the cost side of the copper Debye module is well-formed. Downstream consumers (none yet recorded in the graph) can take cert rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity. In the broader framework this sits under the materials layer that uses the forced $\phi$ (T6) and the J-cost uniqueness (T5) to place laboratory temperature scales on the $\phi$-ladder. Status is structural: the 6% Debye mismatch is reported, not closed, by this certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.