cert
plain-language theorem explainer
Packages three structural facts about the materials-domain cost at recognition rung 33 into one certificate record: diagonal vanishing, nonnegativity for positive arguments, and a positive canonical threshold. Materials or RS auditors cite it as the inhabited structural certificate for this module. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a structural materials certificate at rung 33 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
This module states a structural Recognition Science prediction for the Materials domain at recognition rung 33. Status is a structural theorem pack: zero sorry, zero axiom. The local cost is a domain-level specialization of the RS J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$), restricted to materials observables.
The certificate structure bundles three Prop fields: diagonal vanishing of the domain cost, nonnegativity on the positive quadrant, and positivity of a canonical threshold used as a decision cutoff. Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The materials fields here are the domain-level analogues of that fact plus the identity minimum on the diagonal.
proof idea
One-line structure construction. The definition fills the three fields of the certificate structure by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is performed; inhabitation is pure packaging of already-proved domain facts.
why it matters
Gives the Materials module a single named certificate object for rung-33 structural claims, matching the Plan v7 structural-certificate pattern used across RS domain modules. Downstream use is not yet wired in this graph (no used_by edges), but the sibling cert_inhabited and any future materials forcing or threshold comparisons are the natural consumers.
In the broader framework this sits downstream of J-uniqueness (T5) and the nonnegativity of recognition cost: the domain cost inherits the J-cost minimum at matched arguments and stays nonnegative off-diagonal. It does not itself force phi, the eight-tick octave, or $D=3$; those live in the UnifiedForcingChain. Its role is domain packaging, not foundation forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.