cert
plain-language theorem explainer
Packages three elementary facts about the Module-12 domain cost and threshold into the materials certificate for BCS coherence lengths. Anyone citing the cuprate/conventional ξ match (φ^7 nm and φ^15 nm) uses this bundle. The definition is a pure structure inhabitant: it wires three already-proved sibling lemmas into the certificate fields.
Claim. There is a materials certificate for RS Module 12 whose fields assert: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments; (iii) the canonical threshold is strictly positive.
background
Module 12 of the materials layer records the BCS coherence-length match: $\xi=\varphi^7,\mathrm{nm}\approx 29,\mathrm{nm}$ for cuprates and $\xi=\varphi^{15},\mathrm{nm}\approx 1364,\mathrm{nm}$ for conventional superconductors. The module is marked structural (zero sorry, zero axiom).
The certificate type RSMatl012Cert is a triple of propositions about a real-valued domain cost and a positive threshold. Domain cost is the local cost functional on mass/energy-like pairs; vanishing on the diagonal means equal arguments incur zero cost, and nonnegativity is the standard J-cost lower bound. The upstream forcing result states that every recognition event has nonnegative cost via $J$-cost nonnegativity at positive state.
proof idea
One-line structure inhabitant. Each field is filled by a sibling lemma already proved in the same module: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg, and threshold positivity by canonicalThreshold_pos. No extra algebra is performed at this site.
why it matters
Gives a single named certificate object for the Module-12 materials claims so downstream materials or audit code can demand one inhabitant rather than three separate lemmas. The module doc ties the content to the BCS coherence match on the $\varphi$-ladder ($\varphi^7$ and $\varphi^{15}$ nanometre scales). No used_by edges are recorded yet; the immediate consumer is the companion inhabitation lemma in the same file. In the broader RS chain this sits in the materials layer rather than the T0–T8 forcing core, but it reuses the nonnegative cost discipline from observer forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.