cert
plain-language theorem explainer
Packages three structural facts about the materials domain cost into a single certificate: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy scales, and the canonical threshold is strictly positive. Materials-module consumers cite this inhabited record rather than the three lemmas separately. Construction is a pure field-wiring of sibling proofs.
Claim. There is a materials structural certificate whose fields assert: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive mass and energy scales $m,e$, the domain cost $\mathrm{domainCost}(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 9 of the materials structural layer sits on the RS forcing chain T5 (J-uniqueness) through T8 ($D=3$). Status is a structural theorem block: zero sorry, zero axioms. The local cost is a two-argument domain cost on real mass and energy scales, built from the Recognition Science J-cost (the unique symmetric cost $J(x)=(x+x^{-1})/2-1$).
The certificate structure bundles three Prop fields: diagonal vanishing (equal arguments give cost zero), nonnegativity on the positive quadrant, and positivity of a canonical threshold constant used as a materials cutoff. Upstream, the foundation lemma cost_nonneg already records that every recognition-event cost is nonnegative via $J\ge 0$; the materials nonnegativity field is the corresponding statement for the domain-cost specialization.
Sibling lemmas in the same file discharge each field: diagonal identity, nonnegativity, and threshold positivity.
proof idea
Pure structure instance. The three fields of RSMATStructural009Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or tactics: a one-line field-wiring definition.
why it matters
Gives the materials layer a single named certificate object rather than three loose lemmas, matching the structural-theorem pattern used across RS modules. The module header ties the block to the forcing chain T5 J-uniqueness through T8 three spatial dimensions, so this certificate is the materials-side witness that the domain cost inherits the J-cost minimum and positivity properties forced earlier in the chain.
No downstream consumers are recorded yet (used_by empty). The sibling cert_inhabited likely just re-exports inhabitance of this record. The declaration closes no open scaffold; it is the packaging step after the three field lemmas are already proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.