cert
plain-language theorem explainer
A packaged witness that the Materials-domain structural certificate at recognition rung 93 is inhabited. It records three facts: domain cost vanishes on the equal-argument diagonal, is nonnegative for positive inputs, and the canonical threshold is positive. Materials theorists citing the RS structural prediction at rung 93 use this bundle. The body is a pure structure assembly from three sibling lemmas.
Claim. There exists a Materials structural certificate at recognition rung 93: for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; for all positive $m,e$, one has $C(m,e)\ge 0$; and the canonical threshold $T$ obeys $T>0$.
background
This module states the Recognition Science structural certificate for the Materials domain at recognition rung 93 (Plan v7, 120th pass). Status is structural theorem: zero sorry, zero axiom. The certificate is a three-field structure whose fields are pure cost and threshold properties of the domain cost functional.
Domain cost is the Materials specialization of the RS cost: it is built from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique cost forced by the Recognition Composition Law. Upstream, cost_nonneg in ObserverForcing records that every recognition event has nonnegative cost, via nonnegativity of $J$ on positive reals. The canonical threshold is the positive cutoff against which domain cost is compared in the structural prediction.
Sibling lemmas already prove diagonal vanishing, nonnegativity on the positive quadrant, and positivity of the threshold; this definition only packages them.
proof idea
Definitional structure construction, not a tactic proof. The three fields of StructMaterialsM93Cert are filled by the corresponding sibling results: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No further rewriting or case analysis occurs.
why it matters
Closes the structural certificate for Materials at rung 93 by exhibiting an explicit inhabitant. The module frames this as the RS structural prediction for that domain and rung; the certificate is the formal object that downstream material-ladder or threshold arguments would consume. It sits in the Materials domain of the monolith and inherits nonnegativity from the global J-cost story (T5 J-uniqueness and the RCL). No used_by edges are recorded yet, so its immediate consumers are local (e.g. inhabitedness of the certificate type). It does not itself derive masses, couplings, or experimental materials numbers; it only locks the cost-threshold skeleton at this rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.