cert
plain-language theorem explainer
Canonical witness that the solvation-domain cost vanishes on equal positive scales, stays nonnegative, and that the canonical threshold is strictly positive. Anyone assembling Marcus-style outer reorganization in RS units cites this bundle. It is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate packing three facts about the solvation-domain cost $C$: (i) $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
The module develops RS chemistry as a structural theorem (zero sorry, zero axiom). Marcus outer reorganization energy is $\lambda_{\mathrm{outer}}=(e^2/2)(1/a-1/d)(1/n^2-1/\varepsilon)$. In RS units, at recognition distance $d=\varphi\cdot a$, this collapses to a multiple of the J-cost of $\varphi$ times a charge unit, read as recognition of the solvation shell.
The domain cost $C(m,e)$ is the RS cost comparing medium and environment scales. The structure SolvReorg4Cert packages the three elementary properties needed before any threshold comparison: diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. Upstream, nonnegativity of recognition-event cost is already known from the observer-forcing layer via $J$-cost nonnegativity.
proof idea
One-line structure instance. Field cost_at_eq is filled by the sibling lemma that domain cost vanishes when both arguments equal a nonzero scale. Field cost_nonneg is filled by the sibling nonnegativity lemma for positive medium and environment. Field threshold_pos is filled by positivity of the canonical threshold. No extra algebra is performed here.
why it matters
This certificate is the packaged hypothesis bundle for the RS reading of Marcus outer reorganization: once diagonal vanishing, cost nonnegativity, and a positive threshold are in hand, one can compare domain cost against the threshold and identify $\lambda_{\mathrm{outer}}$ with $J(\varphi)$ times the charge unit at $d=\varphi\cdot a$. That identification sits on the forcing chain landmarks T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point). No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited only records that the type is nonempty. The declaration closes the structural side of session-3 chemistry rather than a dynamical rate law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.