domainCost
plain-language theorem explainer
Defines the domain cost of a pair of reals (m, e) as the RS recognition cost of their ratio m/e. Anyone working the Euler-number structural layer in Foundation cites this as the cost of placing mass or scale m against base e. The body is a one-line abbreviation of the unique J-cost on the positive ratio.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$ on $x>0$).
background
The module treats Euler's number $e$ inside Recognition Science as a structural object (status: structural theorem, zero sorry, zero axiom). The ambient cost is the J-functional forced by the Recognition Composition Law and uniqueness step T5: $J(x)=\frac12(x+x^{-1})-1$ for positive ratios. Upstream copies of Jcost state the same formula and note that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is the unique cost forced by RCL.
Domain cost simply specializes that functional to the ratio of two reals $m$ and $e$. In the RS reading, $m$ is a scale or mass-like quantity and $e$ is the Euler base against which the domain is measured; the cost vanishes only when $m=e$ (ratio one).
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into the already-defined J-cost. No tactics, no lemmas, no hypotheses.
why it matters
Gives the local cost primitive for the Euler-number structural package in Foundation. Sibling results build on it: non-negativity of domain cost, evaluation identities, the canonical threshold, and the Euler-number certificate EulerNumberERS / cert. Framework-wise it sits on T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; without a named cost of $m$ against $e$, the later threshold and certificate statements have nothing to measure. No downstream edges are recorded yet; the immediate consumers are the in-module lemmas that close the structural theorem for $e$ in RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.