RSMatl012Cert
plain-language theorem explainer
Packages three elementary cost and threshold properties required by Materials Module 12 (BCS coherence lengths on the phi ladder). Anyone citing the module's inhabited certificate or the cuprate/conventional xi match uses this bundle. It is a pure structure definition: three named Prop fields, no proof body.
Claim. A certificate consists of three facts: (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
Materials RS Module 12 treats BCS coherence lengths as phi-ladder quantities: $\xi\sim\varphi^7,\mathrm{nm}\approx 29,\mathrm{nm}$ for cuprates and $\xi\sim\varphi^{15},\mathrm{nm}\approx 1364,\mathrm{nm}$ for conventional superconductors, reported as a structural match with zero sorry and zero axiom.
The local cost is a two-argument domain cost on reals (sibling domainCost), expected to sit at the J-cost minimum when the two arguments agree. Nonnegativity of recognition cost is the standard foundation fact: "The cost of any recognition event is non-negative," proved from $J$-cost nonnegativity on positive states. The canonical threshold is a positive real cutoff used by the module's matching criterion.
This structure does not compute $\xi$; it only records the cost/threshold hygiene the certificate constructor must supply.
proof idea
No proof: the declaration is a structure with three Prop fields. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Those lemmas are the actual work; this type only names the interface.
why it matters
Gives Module 12 a single certificate type so downstream code can demand cost diagonal vanishing, cost nonnegativity, and a positive threshold in one place. Immediate consumers are cert (the concrete witness) and cert_inhabited (Nonempty of the certificate). That inhabitedness is what backs the module status line "STRUCTURAL THEOREM (0 sorry, 0 axiom)" for the BCS $\xi$ match against $\varphi^7$ and $\varphi^{15}$ nanometer scales. In the broader RS stack this is materials-side bookkeeping on top of the J-cost calculus (T5 uniqueness, RCL), not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.