domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the recognition cost of their ratio m/e under the unique J-functional. Cite it when comparing scales inside the RS count-law module (2^D-1=7 at D=3). The body is a one-line specialization of Jcost; no proof content.
Claim. For real numbers $m$ and $e$, define the domain cost by $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
Foundation RS Module 7 records the count law $2^D-1=7$ independent observable categories at spatial dimension $D=3$, stated as a structural theorem with zero sorry and zero axioms. The ambient cost is the J-functional forced by T5 uniqueness: $J(x)=\frac{1}{2}(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream snippets fix the same formula in Cost, Cosmology.RefineTrigger, and Gravity.CoherenceCollapse; a genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative on positive arguments.
Domain cost simply evaluates that functional on the quotient of two reals, so a pair $(m,e)$ is scored by how far $m/e$ sits from unity on the recognition scale.
proof idea
Definitional abbreviation only: set domainCost(m,e) equal to Jcost(m/e). No tactics, no lemmas, no obligations. Downstream siblings (nonnegativity, evaluation at equality) inherit the algebraic properties of J directly from this wrapper.
why it matters
Local primitive for Module 7's certificate stack (canonicalThreshold, RSForcingChain007Cert, and the inhabited cert). It packages the T5 J-cost so the count-law development can talk about mass/energy-style ratios without repeating the formula. The module goal is the exact identity $2^D-1=7$ at $D=3$ (forcing-chain landmark T8), and this def supplies the cost language used by sibling lemmas domainCost_nonneg and domainCost_at_eq. The dependency graph lists no external used_by edges, so its role is internal scaffolding for the structural theorem rather than a cross-module export. It does not itself force phi, the eight-tick octave, or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.