cert
plain-language theorem explainer
Packages the three structural obligations for the Materials domain at recognition rung 73 into a single certificate record: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Materials and RS auditors cite it as the inhabited witness that the module's structural claims hold with zero sorry. The body is a pure structure constructor wiring three local lemmas.
Claim. There is a structural materials certificate at recognition rung 73 whose fields assert: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module states a structural Recognition Science prediction for the Materials domain at recognition rung 73 (Plan v7, 120th pass). Status is structural theorem: zero sorry, zero axiom. The certificate type bundles three Prop-valued obligations that any such structural claim must discharge.
Domain cost is the Materials-side cost functional on pairs of positive reals (mass-like and energy-like coordinates). Its diagonal vanishing and off-diagonal nonnegativity mirror the global J-cost geometry: the recognition cost $J$ is minimized at identity and stays nonnegative, as in the upstream fact that every recognition event has nonnegative cost via $J$-cost nonnegativity.
The canonical threshold is the positive cutoff used to separate certified structural regimes from non-certified ones in this domain. Sibling lemmas already prove diagonal vanishing, nonnegativity, and threshold positivity; the certificate only packages them.
proof idea
One-line structure construction. The definition is noncomputable def cert : StructMaterialsM73Cert with three field assignments: cost_at_eq from domainCost_at_eq, cost_nonneg from domainCost_nonneg, and threshold_pos from canonicalThreshold_pos. No further tactics or rewriting; it is pure record assembly of already-proved local facts. Upstream cost_nonneg on recognition events supplies the conceptual template that domain-level nonnegativity follows the same J-cost pattern.
why it matters
Gives the Materials domain an explicit, inhabited structural certificate at rung 73, matching the module claim of a structural RS prediction with empty axiom and sorry surface. Downstream the sibling cert_inhabited (and any future materials forcing or audit lemmas) can point at this value rather than re-proving the three obligations. In the broader framework it is a domain-level instance of the same cost geometry forced by T5 J-uniqueness and the Recognition Composition Law: cost vanishes only on matched ratios and stays nonnegative elsewhere, with a positive threshold marking the certified band. No parent theorem currently depends on it in the graph; it is the terminal witness for this module's structural pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.