cert
plain-language theorem explainer
Packages a materials-domain certificate: the domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical Mott threshold is positive. Anyone citing the RS Mott U/t match (phi^3 in the experimental 3-5 band) would point here. The body is a structure instance that fills three already-proved field lemmas.
Claim. There is a certificate asserting three facts about the materials domain cost $C$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical Mott threshold $T_*$ satisfies $T_*>0$.
background
Materials RS Module 10 treats the Mott metal-insulator transition ratio $U/t$. Recognition Science predicts the dimensionless value $\varphi^3\approx 4.24$, which sits inside the experimental window $3$--$5$; the module is marked MATCH and is a structural theorem (no sorry, no axioms).
The local cost is a two-argument domain cost $C(m,e)$ built from the Recognition J-cost $J(x)=(x+x^{-1})/2-1$. Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J\ge 0$. The certificate structure RSMatl010Cert packages the three elementary properties needed before any threshold comparison: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of the canonical threshold.
proof idea
Definitional structure instance, not a tactic proof. The three fields of the certificate are filled by the sibling lemmas already established in-module: diagonal vanishing of the domain cost, nonnegativity of the domain cost for positive arguments, and positivity of the canonical threshold. No further algebraic work occurs at this site.
why it matters
This is the inhabiting witness for the Module-10 certificate structure. Downstream consumers (none yet linked in the graph) can treat the Mott-side cost axioms as a single named package rather than three separate hypotheses. Within the Recognition chain it sits under the materials layer that compares $\varphi$-ladder thresholds to condensed-matter ratios; the module claim is the Mott $U/t$ match at $\varphi^3$. It does not itself derive $\varphi^3$ from T5--T6; it only certifies the cost/threshold scaffolding those comparisons rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.