cert
plain-language theorem explainer
Packages the three structural facts for the Materials domain at recognition rung 63 into a single certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Materials and RS-certificate consumers cite it as the inhabited witness for the rung-63 materials structure. The body is a pure field assembly from three already-proved sibling lemmas.
Claim. There is a structural materials certificate at recognition rung 63 consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Materials domain at recognition rung 63 (Plan v7, 120th pass), with status STRUCTURAL THEOREM (0 sorry, 0 axiom).
The certificate structure bundles three properties of the domain cost and threshold: equality to zero when the two arguments coincide (and are nonzero), nonnegativity for positive mass and energy arguments, and positivity of the canonical threshold used as the decision cutoff in this domain.
Upstream, nonnegativity of recognition cost is the general fact that every recognition event has nonnegative cost, via nonnegativity of the J-cost on positive states. Here that idea is specialized to the materials domain cost rather than a generic recognition event.
proof idea
One-line structure instance: each of the three fields is filled by the corresponding in-module lemma (domainCost_at_eq, domainCost_nonneg, canonicalThreshold_pos). No additional rewriting or case analysis occurs in this declaration.
why it matters
Gives an inhabited structural certificate for Materials at rung 63, so downstream material or multi-domain certificate consumers can treat the three cost/threshold facts as a single named witness rather than three loose lemmas. It sits in the materials branch of the RS structural-certificate program (rung-indexed domain predictions), not in the T0–T8 forcing chain itself. No used_by edges are recorded yet; the companion cert_inhabited sibling is the natural next consumer. Closes the packaging step for this module’s structural theorem status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.