domainCost
plain-language theorem explainer
Domain cost maps a pair of reals (m, e) to the recognition cost of their ratio m/e. Structural and mass-ladder arguments in Recognition Science cite it whenever a dimensionless mass-to-energy argument is fed to J. The body is a one-line definitional wrapper around the unique RS cost functional.
Claim. For $m,e\in\mathbb{R}$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition Science cost on ratios.
background
The Recognition Composition Law forces a unique cost on positive ratios: $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. This is the T5 landmark (J-uniqueness) in the forcing chain. Upstream packages state the same functional as the RS recognition cost of a positive ratio, and record that a genuine distinction (ratio not one) has strictly positive cost.
This module (Mathematics RS Structural Module 2) collects structural facts about that cost, including the golden-ratio value $J(\varphi)=\varphi-3/2\approx 0.11803$. Domain cost specializes $J$ to a mass-energy ratio $m/e$, the natural dimensionless input when a mass scale is compared to an energy scale in RS-native units ($c=1$).
proof idea
Definitional wrapper only: the right-hand side is exactly $J(m/e)$. There is no tactic proof and no lemma application. Analytic content (nonnegativity, evaluation at special points, thresholds) lives in sibling results that unfold this abbreviation.
why it matters
Names the mass-energy instance of the T5 J-cost inside the structural certificate layer of the module. Sibling facts (equality-at-ratio, nonnegativity, the canonical threshold, and the module certificate) are stated in terms of this abbreviation. In the broader framework it is the local hook for feeding a mass-to-energy ratio into the RCL-forced cost, consistent with the module claim that $J$ is minimized at $\varphi$ with value $\varphi-3/2$. No external downstream uses are recorded yet; the definition exists to keep the structural certificate readable and unit-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.