canonicalThreshold
plain-language theorem explainer
Defines the canonical ionic-strength threshold as φ − 3/2 in RS units. Chemists working the electrolyte-activity certificate cite it as the fixed comparison scale against which domain cost is measured. The body is a pure constant abbreviation; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
The module develops electrolyte solution activity from the Recognition Science J-cost. Activity coefficients satisfy $\log\gamma = J(\varphi)\cdot C_{\mathrm{DH}}\cdot\sqrt{I}$ in the Debye–Hückel regime, with the structural identity that at ionic strength $I=J(\varphi)^2$ one obtains $\log\gamma=-J(\varphi)^3\approx-0.00164$.
Here $\varphi$ is the unique positive fixed point forced by T6 of the unified forcing chain, and $J(x)=(x+x^{-1})/2-1$ is the unique cost functional from T5 / the Recognition Composition Law. The constant $\varphi-3/2$ supplies a dimensionless yardstick on the same scale as those J-values, against which domain cost and positivity certificates are compared.
proof idea
Definitional constant: the real phi - 3/2 is named and exposed. No tactics, no lemmas. Downstream positivity (canonicalThreshold_pos) and the ESSolution5 certificate simply unfold this abbreviation.
why it matters
Gives the Chemistry.ESSolution5 stack a single named scale for the structural activity theorem (Plan v7, 120th pass). The module claims a zero-sorry, zero-axiom certificate that $\gamma\to 1$ at infinite dilution and that the J-cost form of Debye–Hückel is forced. Anchoring the threshold at $\varphi-3/2$ keeps every comparison inside RS-native units (c=1, $\hbar=\varphi^{-5}$) and ties the chemistry layer to T5–T6 of the forcing chain. Sibling lemmas on domain cost non-negativity and the inhabited certificate consume this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.