domainCost
plain-language theorem explainer
Domain cost assigns the RS recognition cost of a mass-to-energy (or scale-to-scale) ratio: J(m/e). Milestone and domain-coverage arguments in the physics layer cite it as the local cost of a pair of real scales. The body is a one-line definition that feeds the quotient into the standard J-cost functional.
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 cost of a positive ratio.
background
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream modules record that a genuine distinction (ratio not one) has strictly positive cost and that $J$ is nonnegative on positive reals. That functional is forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain.
This module is the structural milestone FinalModule_1396 (Plan v7, 109th pass): a zero-sorry, zero-axiom certificate for domain coverage. Domain cost is the local primitive that turns a pair of real parameters into a single nonnegative cost of their ratio, ready for threshold and certificate lemmas in the same file.
proof idea
Pure definition, not a proof. The body applies the shared noncomputable J-cost to the quotient $m/e$. No tactics, no lemmas, no side conditions are discharged at this declaration; positivity and well-definedness for $e\neq 0$ are left to downstream lemmas that constrain the domain.
why it matters
Gives the physics layer a named cost of two real scales so domain-coverage milestones can speak in RS-native units rather than ad hoc ratios. It sits under the J-uniqueness landmark (T5) and the RCL identity that forces $J$. Sibling declarations in the same module (equality at a point, canonical threshold positivity, MilestoneCert) are the natural consumers; the module doc frames the whole file as a structural certificate for domain coverage. No downstream edges are recorded yet, so its role is local scaffolding for those certificate objects rather than a global theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.