RSMATStructural007Cert
plain-language theorem explainer
Certificate record packaging three structural properties of the materials-domain recognition cost: it vanishes when both arguments equal a nonzero scale, it is nonnegative for positive arguments, and the canonical threshold is strictly positive. Materials and RS-cost consumers cite the inhabited instance. Pure structure definition; proofs live in the field witnesses.
Claim. A structural certificate is a triple of assertions: (i) for every nonzero real $r$, the domain cost of the pair $(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
Module RS_MAT_Structural_007 treats ratio symmetry of the Recognition Science J-cost: $J(x)=J(1/x)$, so recognition cost depends only on the scale-free ratio. Status is structural (no sorry, no axioms).
The domain cost is the materials-facing cost functional on a pair of positive reals (mass-like and energy-like scales). Its diagonal vanishing encodes perfect match at equal arguments; nonnegativity is the materials shadow of the global fact that every recognition event has nonnegative cost. The canonical threshold is the positive cutoff used to separate matched from unmatched configurations in this module.
Upstream, ObserverForcing records that the cost of any recognition event is nonnegative via $J$-cost nonnegativity on positive states. That global nonnegativity is the pattern mirrored by the domain-cost field here.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is separate. The concrete witness cert fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then packages that witness as Nonempty.
why it matters
Gives a single named bundle for the three structural claims of Materials module 7 (J-cost ratio symmetry and the associated domain-cost calculus). Downstream, cert is the canonical inhabitant and cert_inhabited proves the type is nonempty, so later materials lemmas can assume one certificate rather than three loose hypotheses.
Fits the RS forcing picture where T5 fixes $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), which is symmetric under $x\mapsto 1/x$ and minimized at $x=1$. Diagonal vanishing and nonnegativity are the materials-level echo of that minimum. No open scaffold: the module is marked structural with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.