domainCost
plain-language theorem explainer
Domain cost of two reals m and e is the recognition cost of their ratio m/e. Anyone comparing Euler's base against a measure (mass, count, or scale) in the RS Euler–phi module cites this wrapper. It is a one-line definitional alias of the standard J-cost on the quotient.
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$.
background
The module treats structural links between Euler's number $e$ and the golden ratio $\varphi$ inside Recognition Science. Status is a structural theorem block (no sorry, no axioms). The working cost is the J-functional $J(x)=\frac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law (forcing step T5): it vanishes only at ratio one and is nonnegative on positive reals.
Domain cost simply evaluates that functional on the ratio of two reals. In the local narrative those arguments are a measure $m$ and the Euler base $e$, so later lemmas can ask whether the cost of placing $m$ against $e$ clears a canonical threshold on the $\varphi$-ladder.
Upstream, every import path resolves to the same $J$ definition (Cost, Cosmology, Gravity bridges, SpiralField).
proof idea
Definitional abbreviation only. The body is the single application Jcost (m / e); there is no tactic proof and no lemma invocation beyond the imported J-cost symbol.
why it matters
Local building block for the Euler–phi certificate stack in the same file (nonnegativity of domain cost, the canonical threshold, and EulerPhiCert). It packages the T5 J-cost so the module can compare $e$ against $\varphi$-powers without rewriting the cost formula at every call site. The module doc frames the open structural question: $e$ and $\varphi$ are transcendentally independent, yet RS seeks a cost-level relation (limit form of $(1+1/n)^n$ versus J). No external used-by edges are recorded yet; the definition exists to keep that comparison uniform inside the structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.