cert
plain-language theorem explainer
Packages three structural facts for the electrolyte J-cost model into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone checking the infinite-dilution activity limit in RS chemistry. Construction is a three-field record fill from sibling lemmas already proved in-module.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats electrolyte-solution activity as a J-cost phenomenon. In Recognition Science the cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. Activity is written structurally as $\log\gamma=J(\varphi)\cdot C_{\mathrm{DH}}\cdot I^{1/2}$, so $\gamma\to 1$ at infinite dilution, and at ionic strength $I=J(\varphi)^2$ one obtains the numerical anchor $\log\gamma=-J(\varphi)^3\approx-0.00164$.
domainCost is the local cost on the mass-energy pair used by this chemistry layer; the certificate structure ESSolution5Cert packages the three algebraic properties needed before any Debye-Hückel-style expansion: diagonal vanishing, nonnegativity, and a positive threshold. Upstream, nonnegativity of recognition cost is the general fact that every recognition event has $J$-cost $\ge 0$ (via Cost.Jcost_nonneg).
proof idea
One-line structure inhabitant. The three fields of ESSolution5Cert are filled by the in-module lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra tactics or rewriting; the definition is pure record assembly.
why it matters
Gives a single named witness that the electrolyte domain cost is a legitimate RS cost (zero on identity pairs, nonnegative, with a positive scale). That is the structural prerequisite for the module claim that activity coefficients arise from $J$-cost and recover $\gamma\to 1$ at infinite dilution, including the concrete evaluation $\log\gamma=-J(\varphi)^3$ at $I=J(\varphi)^2$.
No downstream consumers are wired yet in the graph; the certificate sits as the export point for later chemistry theorems that need a bundled cost hypothesis rather than three separate lemmas. It sits downstream of the general cost-nonnegativity fact from ObserverForcing and of T5 $J$-uniqueness in the forcing chain, without reopening those foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.