domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost J to the dimensionless ratio of a mass parameter m to an energy scale e. Anyone working the structural side of RS cost bounds or threshold comparisons will cite it. The body is a one-line abbreviation of Jcost at m/e; there is no separate argument.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the recognition cost of a positive ratio.
background
The ambient module is Foundation RS Structural Module 6, whose theme is phi uniqueness: phi as the self-similar fixed point of the continued fraction $1+1/(1+1/\cdots)$, recorded as a structural theorem with no sorry and no axiom.
The only primitive used here is the recognition cost $J$. Across Cost, Cosmology, Gravity, and Spiral it is the same functional: $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ for $x > 0$. Upstream docs call it "the RS recognition cost of a positive ratio" and "the unique cost functional forced by the Recognition Composition Law." A genuine distinction (ratio not one) has strictly positive cost; $J$ is nonnegative on positives.
Domain cost simply specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when comparing a mass parameter against a local energy or threshold scale.
proof idea
Definition only: the body is the single application Jcost (m / e). No tactics, no lemmas, no cases. Downstream facts such as nonnegativity or evaluation identities are proved separately from properties of $J$.
why it matters
In the Recognition framework the cost $J$ is the T5 landmark: the unique functional forced by the Recognition Composition Law, equivalently $J(x) = \cosh(\log x) - 1$. Packaging $J(m/e)$ as domain cost gives Structural Module 6 a named hook for mass-versus-energy comparisons that sit next to phi uniqueness and the self-similar fixed point (T6).
No downstream theorems currently depend on this def in the graph (used_by is empty). Sibling declarations in the same module (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, and the module certificate) are the immediate consumers: they turn the abbreviation into nonnegativity, evaluation lemmas, and a structural certificate. The def itself does not close an open question; it is scaffolding vocabulary for those results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.