domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science cost of a mass-to-energy ratio: J(m/e) with the unique J forced by the composition law. Chemists and RS foundation readers cite it when mapping Marcus outer reorganization energy onto recognition of a solvation shell. The body is a one-line definition wrapping the standard J-cost on the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the RS recognition cost of a positive ratio.
background
The Chemistry module develops an RS reading of Marcus theory. Classically, the outer reorganization energy is $\lambda_{\mathrm{outer}}=\frac{e^2}{2}\bigl(\frac{1}{a}-\frac{1}{d}\bigr)\bigl(\frac{1}{n^2}-\frac{1}{\varepsilon}\bigr)$. In RS units the natural shell distance is $d=\varphi,a$, and the module claims $\lambda_{\mathrm{outer}}$ collapses to a multiple of $J(\varphi)$ times a charge unit from recognition of the solvation shell.
The cost functional used everywhere is $J(x)=\frac{1}{2}(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the unique cost forced by the Recognition Composition Law, nonnegative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply feeds the dimensionless ratio of a mass-like scale to an energy-like scale into that same $J$.
proof idea
Pure definition: apply the standard J-cost to the quotient $m/e$. No lemmas, no tactics, no hypotheses. Sibling lemmas (nonnegativity, evaluation at equality) are proved separately from the known properties of $J$.
why it matters
This is the local cost primitive for the RS Chemistry session. The module status is structural (zero sorry, zero axiom): it rewrites Marcus outer reorganization at the RS distance $d=\varphi a$ as recognition cost of the solvation shell. Domain cost is the map that turns a mass/energy pair into that J-value, so later certificates (canonical threshold, SolvReorg4Cert) can compare shell costs against $J(\varphi)$ and the golden fixed point from the forcing chain (T5–T6). No downstream users are wired yet in the graph; the definition sits ready for those chemistry certificates and any bridge that needs a ratio cost in foundation units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.