RSMatl009Cert
plain-language theorem explainer
Certificate structure bundling three structural side-conditions for the Pb Cooper-pair materials module: diagonal vanishing of the domain cost, nonnegativity on positive arguments, and positivity of the canonical threshold. Anyone citing the module's phi^3 binding match (0.642 meV to 2.72 meV) relies on this bundle. Pure definitional packaging with no proof body; inhabitants are assembled elsewhere.
Claim. A materials certificate for module 9 is a triple of facts: (i) for every nonzero real $r$, the domain cost at equal arguments vanishes, $C(r,r)=0$; (ii) whenever $m>0$ and $e>0$, the domain cost satisfies $C(m,e)\ge 0$; (iii) the canonical threshold $T$ is strictly positive, $T>0$.
background
Materials RS Module 9 records the Cooper-pair binding scale in lead (Pb) as a phi-ladder match: $\phi^3\cdot 0.642,\mathrm{meV}=2.72,\mathrm{meV}$. Status is structural (zero sorry, zero axiom). The certificate does not restate that numerical claim; it packages the cost-side obligations that underwrite it.
The domain cost is the materials-layer 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$ is the identity minimum at equal mass/energy arguments. Nonnegativity mirrors the foundation fact that every recognition event has nonnegative cost.
Upstream, cost_nonneg in ObserverForcing states: "The cost of any recognition event is non-negative," proved via Jcost_nonneg on the positive state. The canonical threshold is the positive cutoff used to gate the binding comparison in this module.
proof idea
No proof body: this is a structure declaration. It names three fields any inhabitant must supply (diagonal vanishing, nonnegativity, threshold positivity). The concrete lemmas that fill those fields are the sibling results on domain-cost equality at equal arguments, domain-cost nonnegativity, and positivity of the canonical threshold. The downstream definition cert assembles those three lemmas into one inhabitant; cert_inhabited then records nonemptiness.
why it matters
Gives the typed interface that the Pb Cooper-pair module must inhabit. Downstream, cert builds a concrete inhabitant and cert_inhabited proves the type is nonempty, closing the structural side of Module 9 (0 sorry, 0 axiom).
In the broader Recognition framework this sits in the materials layer that connects the phi-ladder (T6 fixed point, mass/energy rungs) to condensed-matter observables. The physical claim underwritten is the Cooper-pair binding match $\phi^3\cdot 0.642,\mathrm{meV}=2.72,\mathrm{meV}$. The certificate itself is only the cost/threshold scaffolding; the numerical MATCH is recorded in the module documentation, not inside these three fields.
Parent use is local to this module: without an inhabited certificate the structural theorem status would not hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.