cert
plain-language theorem explainer
Packages the three structural facts of the Module-7 chemistry cost into one certificate: diagonal vanishing, non-negativity for positive mass/energy, and a strictly positive canonical threshold. Cited by anyone checking Marcus-lambda consistency in RS chemistry. Pure structure inhabitant that wires three already-proved sibling lemmas; no new math.
Claim. There is a Module-7 chemistry certificate recording: (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 $T$ satisfies $T>0$.
background
Chemistry RS Module 7 treats the Marcus reorganization energy (lambda) in Recognition Science units. The module claims the structural identity $J(\varphi)^{-1}\cdot kT=0.22,\mathrm{eV}$ at the inner-sphere minimum, and marks the claim CONSISTENT with a zero-sorry structural theorem.
The domain cost $C$ is the local cost functional on positive real mass/energy coordinates; it is built from the RS $J$-cost $J(x)=(x+x^{-1})/2-1$, which is non-negative and vanishes only at the identity $x=1$. The canonical threshold is the positive cutoff used to separate on-shell from off-shell recognition events in this chemistry layer.
Upstream, cost_nonneg from ObserverForcing states that every recognition event has non-negative cost, via $J$-cost non-negativity. The certificate structure RSChem007Cert simply packages the three algebraic properties the module needs: diagonal vanishing, non-negativity, and threshold positivity.
proof idea
One-line structure inhabitant. The three fields of RSChem007Cert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity on the positive orthant), and canonicalThreshold_pos (strict positivity of the threshold). No tactic proof and no new calculation; pure wiring of already-established facts.
why it matters
Gives a single named certificate that Module 7's Marcus-lambda cost layer is structurally well-formed: cost is a genuine non-negative defect vanishing on matched coordinates, and the threshold that gates the $0.22,\mathrm{eV}$ identity is positive. Downstream consumers (none yet recorded in the graph) can assume cert rather than re-proving the three properties. Sits inside the chemistry specialization of the RS forcing chain: $J$-uniqueness (T5) and the golden ratio $\varphi$ (T6) already fix the cost shape; this module only checks that the chemistry-scale threshold and diagonal identities remain consistent with that shape. Status is structural theorem, zero sorry, zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.