StructMaterialsM33Cert
plain-language theorem explainer
Packages the three structural obligations for the Materials domain certificate at recognition rung 33: diagonal vanishing of domain cost, nonnegativity for positive arguments, and a strictly positive canonical threshold. Downstream code cites it as the type of the concrete witness `cert` and of the inhabitation theorem. Pure structure definition with no proof body.
Claim. A Materials structural certificate at recognition rung 33 is a triple of properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every nonzero real $r$; (ii) the domain cost is nonnegative whenever both arguments are positive; (iii) the canonical threshold is strictly positive.
background
The module states a structural Recognition Science prediction for the Materials domain at recognition rung 33 (Plan v7, 120th pass), marked as a structural theorem with zero sorry and zero axioms.
Domain cost is the Materials specialization of the RS cost functional (imported from Cost and Constants). The first field requires that cost to vanish when both arguments equal the same nonzero real, i.e. on the balanced diagonal. The second field is the Materials-level nonnegativity statement for positive mass and energy parameters. The third field asserts that the module's canonical threshold constant is strictly positive.
Upstream, the foundation lemma cost_nonneg records that every recognition event has nonnegative cost, proved by reducing to nonnegativity of the J-cost on positive reals. That global fact is the template this Materials certificate mirrors at the domain level.
proof idea
No proof: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line theorem that wraps that witness in Nonempty.
why it matters
Gives the typed interface for the Materials rung-33 structural certificate. The concrete witness and the inhabitation theorem both target this structure, so any later Materials argument that needs "the certificate exists" depends on these three obligations being dischargeable.
In the broader RS stack this is a domain-level packaging of cost nonnegativity and a positive threshold, aligned with the foundation fact that recognition costs are nonnegative via J-cost. It does not itself invoke the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3), but it sits in the materials layer that consumes those constants and the cost calculus.
Closes the structural-certificate shape for this module; open physics content lives in how domainCost and canonicalThreshold are defined, not in this bundle type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.