cert
plain-language theorem explainer
Packages the three structural cost axioms for Chemistry Module 8 (Cu Debye temperature on the phi ladder) into a single certificate record. Anyone citing the module's structural status uses this inhabitant. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Chemistry RS Module 8 is a structural claim about the Debye temperature of copper: $\phi^{12}\approx 321.9,\mathrm{K}$ versus the experimental $\sim 343,\mathrm{K}$ (about 6% off). The module is marked structural theorem with zero sorry and zero axioms.
The domain cost is the local recognition cost on the chemistry side, built from the global J-cost $J(x)=(x+x^{-1})/2-1$. Non-negativity of J-cost for recognition events is already established upstream (cost_nonneg: "The cost of any recognition event is non-negative"). The certificate structure RSChem008Cert simply records the three properties a chemistry-domain cost must satisfy: diagonal vanishing, non-negativity on the positive quadrant, and a positive canonical threshold.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new reasoning occurs here; the def only assembles those proofs into the certificate record.
why it matters
Gives the module a single named certificate object that downstream chemistry or ledger code can require as a hypothesis, rather than re-proving diagonal vanishing and non-negativity ad hoc. It sits inside the structural layer of the phi-ladder mass/temperature claims (here Debye $T$ for Cu at rung 12). No parent theorems currently depend on it (used_by is empty), so its role is local packaging for the module's structural status claim. It does not itself close the 6% experimental gap; that remains a numerical comparison outside the Lean kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.