cert
plain-language theorem explainer
Packages three structural facts about the module-9 domain cost into a single certificate for the Pb Cooper-pair binding claim. Anyone citing the lead gap match (phi^3 times 0.642 meV equals 2.72 meV) uses this bundle as the formal witness. The definition is a pure structure inhabitant: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a materials module-9 certificate whose fields assert: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
Module 9 of the materials layer records the Cooper-pair binding energy in lead: $\varphi^3\cdot 0.642,\mathrm{meV}=2.72,\mathrm{meV}$, flagged as a numerical MATCH and a structural theorem (no sorry, no axiom). The local cost is the Recognition Science $J$-cost pulled back to a two-argument domain cost on positive reals; $J(x)=(x+x^{-1})/2-1$ is the unique nonnegative cost fixed by the Recognition Composition Law, minimized at the identity $x=1$.
The certificate structure RSMatl009Cert is the module's formal interface: diagonal vanishing (equal arguments cost nothing), nonnegativity for positive inputs, and a strictly positive canonical threshold against which binding is compared. Upstream, nonnegativity of recognition-event cost is already forced in ObserverForcing via $J\ge 0$.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas already proved in the same module: diagonal vanishing, domain-cost nonnegativity (itself resting on the global $J$-cost nonnegativity theorem), and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
Gives the materials layer a single named witness that the Pb Cooper-pair cost model is well-posed: cost is a true cost (nonnegative, zero on the nose when arguments match) and the comparison threshold is positive. That is the structural half of the module-9 MATCH claim $\varphi^3\cdot 0.642,\mathrm{meV}=2.72,\mathrm{meV}$. In the broader RS chain it sits downstream of $J$-uniqueness (T5) and the forced self-similar scale $\varphi$ (T6), which fix the cost and the rung arithmetic used for the meV figure. No downstream consumers are wired yet; the certificate is the export surface for later materials or condensed-matter corollaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.