RSMatl002Cert
plain-language theorem explainer
Certificate bundle for Materials module 2: the domain cost vanishes on the diagonal, stays non-negative off it for positive arguments, and the canonical threshold is strictly positive. Materials and Debye-temperature arguments cite it as the structural gate before comparing φ^12 K to copper's measured Debye temperature. The structure is pure data; inhabitance is discharged by the sibling lemmas that prove each field.
Claim. A materials-module certificate is a triple of 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 2 is a structural (zero-sorry) layer aimed at the copper Debye temperature: the RS prediction $\phi^{12},\mathrm{K}\approx 321.9,\mathrm{K}$ sits about 6% below the experimental $\sim 343,\mathrm{K}$. Before that numerical comparison is trusted, the module packages three elementary cost and threshold properties as a single certificate type.
The domain cost is the materials-side specialization of the recognition cost (the $J$-cost family from the foundation). Upstream, cost_nonneg in ObserverForcing states that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states. The diagonal vanishing clause is the materials analogue of sitting at the $J$-cost minimum when the two arguments coincide (identity scale). The canonical threshold is the positive cutoff used later to gate the Debye comparison.
Sibling lemmas in the same module prove each field separately: diagonal identity of the domain cost, its nonnegativity for positive mass/energy-like arguments, and positivity of the canonical threshold.
proof idea
No proof body: this is a structure definition, not a theorem. It records three propositions as fields. Downstream, the noncomputable value cert fills those fields by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitance is then the one-line ⟨cert⟩.
why it matters
The certificate is the typed gate for Materials module 2. Downstream, cert inhabits it and cert_inhabited records Nonempty RSMatl002Cert, so later materials arguments can assume the cost axioms and a positive threshold without re-proving them. In the broader RS stack this sits under the $J$-cost nonnegativity and identity-minimum story (T5 $J$-uniqueness, RCL), specialized to a materials domain cost rather than a generic recognition event. The module's scientific target is the structural Debye match $\phi^{12},\mathrm{K}$ versus copper; the certificate does not itself compute that number, but it is the precondition package the module exposes before any such comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.