cert
plain-language theorem explainer
Packages three structural facts about the H-bond domain cost into one certificate: it vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Anyone auditing the Module-5 claim that H-bond energy sits at J(φ)^{-1} kT N_A ≈ 20.8 kJ/mol would cite this bundle. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) the chemistry domain cost satisfies $\mathrm{cost}(r,r)=0$ for every nonzero real $r$; (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Chemistry RS Module 5 targets hydrogen-bond energy. In RS-native units the predicted scale is $J(\varphi)^{-1},kT,N_A$, numerically about 20.8 kJ/mol, which lies in the empirical H-bond band. The module is marked a structural theorem (no sorry, no axioms).
The domain cost is the local cost functional used for this chemistry claim. It is built from the global recognition cost $J$, the unique solution of the Recognition Composition Law forced at T5, with $J(x)=(x+x^{-1})/2-1$. Nonnegativity of $J$ (and thus of event costs) is the upstream fact cost_nonneg from ObserverForcing: every recognition event has cost $\ge 0$.
The certificate structure simply records the three properties the rest of the module needs: diagonal vanishing, positivity of cost off the identity, and a positive comparison threshold.
proof idea
Pure structure inhabitation. The three fields of RSChem005Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass/energy arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra or tactics; the def is the witness.
why it matters
This is the single packaged witness that Module 5's cost side is well-formed before any numerical H-bond comparison is trusted. It sits under the module claim that $J(\varphi)^{-1} kT N_A$ lands in the H-bond energy window (~20.8 kJ/mol) and is consistent. The nonnegativity leg ultimately rests on T5 J-uniqueness and the global cost-nonnegativity theorem. No downstream consumers are recorded yet; the cert is the local closure object for the structural side of the chemistry claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.