RSMATStructural010Cert
plain-language theorem explainer
A certificate packing three structural facts for materials-domain cost: the cost vanishes on equal arguments, stays non-negative for positive mass and energy scales, and the canonical threshold is strictly positive. Materials and calibration proofs cite it as the single interface for those inequalities. It is a pure structure definition; inhabitance is discharged elsewhere by the concrete lemmas on domain cost and the threshold.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the materials domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e>0$, $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
This module is Materials RS Structural Module 10. The local setting is RS calibration with the coherence energy $E_{\mathrm{coh}}$ fixed once by the electron mass, after which materials predictions are parameter-free. The status line marks the module as a structural theorem block with no sorry and no axioms.
The domain cost $C$ is the materials-side cost functional (built from the Recognition Science $J$-cost). Upstream, the foundation result cost_nonneg states that the cost of any recognition event is non-negative, via non-negativity of $J$. The certificate isolates the three inequalities the materials layer needs: diagonal vanishing, positivity off the identity, and a positive decision threshold.
Sibling lemmas supply the concrete witnesses: diagonal identity of domain cost, its non-negativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
No proof body: this is a structure definition, not a theorem. The three fields are propositions that any inhabitant must supply. Downstream, the definition cert fills them by pointing at domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then packages that single inhabitant as Nonempty.
why it matters
The certificate is the typed interface for Structural Module 10 in the materials layer. Downstream cert and cert_inhabited show the interface is realized with zero sorry, matching the module claim that calibration is parameter-free once $E_{\mathrm{coh}}$ is fixed by the electron mass.
In the broader Recognition framework this sits under the $J$-cost calculus (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the non-negativity of recognition cost. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it only packages the cost and threshold facts materials proofs need when comparing scales to the canonical threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.