RSMATStructural009Cert
plain-language theorem explainer
Certificate structure bundling three materials-domain cost axioms: diagonal vanishing of domain cost, nonnegativity on positive arguments, and positivity of the canonical threshold. Materials and RS structural consumers cite it via the inhabited instance. Pure structure definition with no proof body; the three fields are discharged by sibling lemmas when the certificate is built.
Claim. A materials structural certificate comprises three statements: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MAT_Structural_009 sits in the Materials layer of the Recognition Science monolith. Its header places it on the forcing chain T5 (J-uniqueness) through T8 (D=3), and marks the file as a structural theorem package with zero sorry and zero axioms.
Domain cost is the local cost functional on pairs of positive reals (mass-like and energy-like coordinates in the materials setting). It is the materials-side avatar of the recognition J-cost: the upstream result cost_nonneg states that every recognition event has nonnegative cost, via Cost.Jcost_nonneg on a positive state. The diagonal identity domainCost r r = 0 for r ≠ 0 is the materials analogue of the J-cost minimum at the identity ratio.
The canonical threshold is a fixed positive real used as a comparison scale for domain-cost values in later structural claims. Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos supply the three fields of this certificate.
proof idea
No proof body: this is a structure declaration whose three fields are propositions. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. The nonempty witness cert_inhabited is then the one-line constructor ⟨cert⟩.
why it matters
This certificate is the typed interface for Materials structural module 9. Downstream, cert builds a concrete inhabitant and cert_inhabited proves Nonempty, so any later lemma that needs the three cost/threshold facts can take an RSMATStructural009Cert rather than re-proving the siblings.
In the RS framework it packages the materials-side consequences of the J-cost calculus (nonnegativity and identity minimum) together with a positive threshold scale, consistent with the module’s placement on the T5–T8 forcing chain. It does not itself advance a new physical prediction; it freezes the structural hypotheses that later materials claims may assume without reopening the cost theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.