domainCost
plain-language theorem explainer
Domain cost scores a pair of real scales by the recognition cost of their ratio: J(m/e). Elastic-modulus and related continuum arguments in RS cite it whenever a modulus must be compared to a reference energy density on the phi-ladder. The body is a one-line abbreviation of the standard J-cost.
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 Science cost of a positive ratio.
background
The module derives a structural elastic-modulus estimate from the phi-ladder (Plan v7, 119th pass). Status is a structural theorem with no sorry and no axioms. The steel benchmark is $E\sim 200,\mathrm{GPa}$; the RS estimate is $\varphi^{10}\cdot 2,\mathrm{GPa}\approx 246,\mathrm{GPa}$, using $\varphi^{10}\sim 123$.
Upstream, $J$ is the unique recognition cost forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Doc-comments record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positive reals. Domain cost simply feeds the ratio of two continuum scales into that functional.
proof idea
Pure definition: one-line abbreviation that applies the standard $J$-cost to the quotient $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the local cost functional used by the ElasticMod4 certificate and its siblings (nonnegativity, evaluation at equality, canonical threshold). In the broader framework it is the continuum avatar of T5 J-uniqueness: moduli and reference energies are compared by the same $J$ that forces $\varphi$ and the eight-tick structure elsewhere. No downstream theorems are wired yet in the graph; the immediate consumers are the in-module lemmas that prove nonnegativity and pin the canonical threshold for the modulus match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.