RSMatl010Cert
plain-language theorem explainer
Certificate bundle for Materials module 10 (Mott U/t): diagonal domain cost vanishes, domain cost is nonnegative for positive arguments, and the canonical threshold is positive. Materials and condensed-matter RS audits cite it as the structural witness that the module is inhabited. The structure itself is pure interface; the concrete inhabitant wires three sibling lemmas.
Claim. A certificate for the Mott-transition materials module consists of three facts: (i) for every nonzero real $r$, the domain cost at equal arguments satisfies $C(r,r)=0$; (ii) for all positive reals $m,e>0$, the domain cost obeys $C(m,e)\ge 0$; (iii) the canonical threshold $T$ (the RS Mott $U/t$ scale) satisfies $T>0$.
background
Materials RS Module 10 targets the Mott transition ratio $U/t$. In Recognition Science the predicted scale is $\varphi^3\approx 4.236$, which sits inside the empirical band $3$–$5$ (module status: structural match, zero sorry, zero axiom).
The domain cost $C(m,e)$ is the materials-side specialization of the recognition $J$-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Diagonal vanishing $C(r,r)=0$ encodes that equal mass/energy (or equal hopping/interaction) arguments sit at the cost minimum. Nonnegativity is the materials lift of the foundation fact that every recognition event has nonnegative cost.
The canonical threshold is the positive real used as the RS Mott $U/t$ yardstick (tied to $\varphi^3$). Upstream, cost_nonneg in ObserverForcing states: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states.
proof idea
No proof body: this is a structure (interface) definition, not a theorem. It packages three Prop fields that any inhabitant must supply: diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold.
The concrete witness cert fills the fields by direct assignment from the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Downstream cert_inhabited is then the one-line Nonempty wrapper ⟨cert⟩.
why it matters
This structure is the formal gate for Materials module 10. Downstream, cert inhabits it and cert_inhabited records Nonempty RSMatl010Cert, closing the module as a structural theorem (0 sorry, 0 axiom) with a Mott $U/t$ match at $\varphi^3\approx 4.24$ in the range $3$–$5$.
In the broader RS chain the cost fields inherit the $J$-uniqueness and nonnegativity story (forcing T5 and the RCL), while the positive threshold anchors the materials prediction to the golden-ratio ladder. The certificate pattern lets later materials modules and audits demand a single inhabited bundle rather than three loose lemmas, keeping the Mott claim machine-checkable without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.