domainCost
plain-language theorem explainer
Domain cost evaluates the Recognition Science J-cost on the dimensionless ratio of a mass parameter to an energy scale. Anyone working the T0–T8 forcing chain or mass-ladder bookkeeping cites it as the local cost of a mass/energy mismatch. The body is a one-line abbreviation of Jcost applied to m/e.
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 RS recognition cost of a positive ratio.
background
Module 5 of the RS forcing chain records structural theorems for T0–T8 with zero sorry and zero axioms. The only primitive cost in play is the J-cost $J(x) = \frac{x + x^{-1}}{2} - 1$, also written $\cosh(\log x) - 1$, forced uniquely at T5 by the Recognition Composition Law.
Upstream, Jcost is defined identically in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse: it is the RS recognition cost of a positive ratio, nonnegative for $x > 0$, and strictly positive when the ratio is not one. Domain cost simply specializes that functional to the ratio of a mass-like parameter $m$ to an energy scale $e$.
Sibling declarations in the same module (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) treat this quantity as the local cost that thresholds and certificates later compare against.
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No tactics, no lemmas, no hypotheses. Downstream proofs that need nonnegativity or evaluation at equality invoke the sibling lemmas rather than re-expanding J.
why it matters
In the forcing chain, every structural comparison of scales is measured by J-cost (T5 uniqueness). Packaging $J(m/e)$ as domain cost gives Module 5 a uniform name for mass-versus-energy mismatch before thresholds and the module certificate are stated.
Although this page lists no direct used-by edges, the sibling cluster (domainCost_nonneg, domainCost_at_eq, canonicalThreshold, RSForcingChain005Cert) is built on top of it. That cluster sits inside the T0–T8 structural spine: J uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, and $D = 3$. The definition itself closes no open question; it is the shared cost interface those later facts consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.