domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the recognition cost of their ratio m/e. It is the local cost functional used in the RS electrolyte-activity model (Debye–Hückel style log-gamma). The definition is a one-line abbreviation of the standard J-cost on the ratio.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module develops electrolyte solution activity from J-cost (Plan v7, structural, zero sorry). The RS claim is that $\log\gamma$ is proportional to $J(\varphi)$ times the Debye–Hückel factor $\sqrt{I}$, so activity coefficients approach 1 at infinite dilution, with a concrete structural value at $I=J(\varphi)^2$.
The underlying cost is the unique T5 functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), imported here as Jcost. Upstream docs state it as the RS recognition cost of a positive ratio, strictly positive when the ratio is not one, and nonnegative for positive $x$.
Domain cost simply specializes that functional to a mass/energy (or concentration) ratio $m/e$, giving a named chemistry-facing wrapper used by the sibling lemmas on nonnegativity and evaluation at equality.
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No proof obligations; the body is the term applying the imported J-cost to the ratio.
why it matters
Gives the chemistry module a named cost on the m/e scale so later certificates (canonical threshold, ESSolution5Cert) can speak about activity without reopening the T5 uniqueness argument. It sits under the Recognition Composition Law and the forced J of the T0–T8 chain: once J is unique, every domain-specific cost is just J of a ratio. The module doc pins the structural target $\log\gamma=-J(\varphi)^3\approx-0.00164$ at $I=J(\varphi)^2$; domain cost is the primitive that makes that identity well-typed. No downstream edges are recorded yet; siblings domainCost_nonneg and domainCost_at_eq are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.