ESSolution5Cert
plain-language theorem explainer
A certificate packing three structural facts for the RS electrolyte-activity model: the domain cost vanishes on equal positive arguments, stays non-negative for positive mass and energy, and the canonical dilution threshold is strictly positive. Chemists and RS auditors cite it when discharging the infinite-dilution limit of the activity coefficient. It is a pure structure definition; inhabitance is supplied separately by wiring the sibling lemmas.
Claim. A certificate for the fifth electrolyte-solution model consists of three properties: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $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 activity coefficient obeys $\log(\gamma)=J(\varphi)\cdot C_{\mathrm{DH}}\cdot I^{1/2}$ (Debye–Hückel form with RS prefactor). At ionic strength $I=J(\varphi)^2$ one obtains the structural value $\log(\gamma)=-J(\varphi)^3\approx-0.00164$, and $\gamma\to 1$ at infinite dilution.
The domain cost is the local cost functional on mass/energy (or concentration) pairs used by this chemistry layer; it is built from the standard nonnegative J-cost $J(x)=(x+x^{-1})/2-1$. The upstream fact that every recognition-event cost is nonnegative (via $J\ge 0$ for positive state) is the template for the domain-cost nonnegativity field.
The canonical threshold is the positive scale at which the RS activity formula is evaluated (tied to $J(\varphi)$). This structure does not prove those facts; it only names the triple of propositions a complete certificate must carry.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Downstream, cert assembles an inhabitant by assigning domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields; cert_inhabited then packages that inhabitant as Nonempty ESSolution5Cert. The mathematical work lives in those sibling lemmas, not here.
why it matters
In the Chemistry.ESSolution5 development this certificate is the typed interface that marks the electrolyte-activity model as structurally closed (module status: 0 sorry, 0 axiom). Downstream cert and cert_inhabited use it to exhibit a concrete witness, so later chemistry results can assume the diagonal-vanishing, nonnegativity, and positive-threshold package without re-proving each piece.
Framework-wise it sits under the J-cost uniqueness and nonnegativity strand (T5 / RCL): activity is read as a recognition cost, so the same $J\ge 0$ and $J(1)=0$ geometry that forces the identity minimum also forces $\gamma\to 1$ at infinite dilution and the numerical RS anchor $\log(\gamma)=-J(\varphi)^3$. It does not itself derive Debye–Hückel phenomenology from first principles; it freezes the cost axioms the activity formula needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.