canonicalThreshold_pos
plain-language theorem explainer
The RS chemistry canonical threshold is a strictly positive real. Anyone working solvation or Marcus-style reorganization certificates in this module needs that positivity as a side condition. The proof is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold constant of the RS chemistry layer is strictly positive: $0 < \tau$, where $\tau$ is defined from the golden ratio $\varphi=(1+\sqrt{5})/2$ and the inequality follows from $\varphi>1.5$.
background
Module status is structural RS chemistry (zero sorry, zero axiom). The local setting rewrites Marcus outer reorganization: classically $\lambda_{\mathrm{outer}}=(e^2/2)(1/a-1/d)(1/n^2-1/\varepsilon)$; in RS, at shell distance $d=\varphi,a$, this collapses to $J(\varphi)$ times a charge unit from recognition of the solvation shell.
The only upstream fact used here is the tighter lower bound $\varphi>1.5$, proved from $\sqrt{5}>2$ so $(1+\sqrt{5})/2>3/2$. Sibling definitions in the same file introduce domain cost, the canonical threshold itself, and the four-point solvation-reorganization certificate that will consume positivity facts of this kind.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0<\tau$ by linarith using the lemma $\varphi>1.5$. No further case splits or cost identities are required; positivity is pure arithmetic once the definition is expanded.
why it matters
Keeps the chemistry layer's threshold well-formed before any domain-cost or solvation-reorganization certificate is stated. Downstream siblings (SolvReorg4Cert, cert, cert_inhabited) sit in the same file and rely on a positive scale when comparing reorganization energy to recognition cost $J$. In the broader forcing chain this is local bookkeeping, not a T0–T8 step, but it ties Marcus outer $\lambda$ at $d=\varphi a$ to the unique $J$-cost and the self-similar fixed point $\varphi$. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.