RSChem005Cert
plain-language theorem explainer
Certificate record for Chemistry Module 5 (H-bond energy band) packing three structural obligations: domain cost vanishes on the diagonal, is non-negative for positive arguments, and the canonical threshold is positive. Downstream code inhabits it via `cert` and proves Nonempty. Pure structure definition with no proof body.
Claim. A Module-5 chemistry certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Chemistry RS Module 5 targets the hydrogen-bond energy scale $J(\varphi)^{-1},kT,N_A\approx 20.8,\mathrm{kJ/mol}$, reported as consistent and as a structural theorem (zero sorry, zero axiom). The local cost is a domain specialization of the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative and minimized at the identity $x=1$.
Upstream, ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states. The module therefore lifts that global fact to a chemistry-facing domainCost on mass/energy pairs, together with a positive canonicalThreshold that marks the H-bond acceptance band.
The certificate structure is the interface those three facts must satisfy before the module can export an inhabited witness.
proof idea
No proof body: this is a structure declaration. Its three fields are Prop-valued obligations. The actual proofs live on the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, which are later packed into the concrete inhabitant cert. Nonnegativity ultimately traces to the upstream cost_nonneg / Jcost_nonneg chain.
why it matters
Gives the typed interface that Module 5 must discharge to claim structural consistency of the H-bond energy window. Downstream, cert fills the three fields from the sibling lemmas, and cert_inhabited records Nonempty RSChem005Cert, closing the module's export surface.
In the broader RS stack this sits under the chemistry layer that reuses the forced J-cost (T5) and the golden ratio $\varphi$ (T6) to fix energy yardsticks; the numerical target $J(\varphi)^{-1} kT N_A$ is the chemistry-facing readout of that ladder. The certificate does not itself compute 20.8 kJ/mol; it only locks the cost and threshold axioms the computation rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.