cert
plain-language theorem explainer
Packages three proved facts about the materials domain cost into a single certificate: vanishing on the diagonal, non-negativity for positive mass and energy, and positivity of the canonical threshold. Materials and RS structural auditors cite it as the inhabited witness for the module-3 certificate type. The body is a pure structure instance, wiring three sibling lemmas into the fields.
Claim. There is a certificate recording that (i) the materials domain cost satisfies $\mathrm{domainCost}(r,r)=0$ for every $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
Module RS_MAT_Structural_003 is the third materials structural block. Its stated content is the RS Count Law $2^D-1=7$ independent channels, forced by the $D=3$ configuration dimension (T8 in the forcing chain). Status is structural: zero sorry, zero axiom.
The certificate type bundles three cost-side obligations used by that materials layer. Domain cost is the local cost functional on mass/energy pairs; the diagonal-vanishing clause says equal arguments incur zero cost, matching the J-cost minimum at identity. Non-negativity is the materials-side shadow of the global fact that every recognition event has non-negative cost (ObserverForcing: "The cost of any recognition event is non-negative"). The canonical threshold is the positive cutoff against which domain costs are compared.
proof idea
One-line structure instance. Each field is filled by a sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, non-negativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra tactics or algebraic work; the definition is pure packaging.
why it matters
Gives an inhabited value of the module-3 materials certificate, so downstream consumers can assume the three cost axioms as a single object rather than three free hypotheses. Sits under the RS Count Law narrative ($2^D-1=7$ channels from $D=3$), which is the materials reading of T8. No used_by edges are recorded yet; the natural consumer is the sibling inhabitance lemma and any later materials theorems that take the certificate as a hypothesis. Closes the definitional side of a zero-sorry structural module rather than a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.