domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition cost of their ratio: J(m/e). ConfigDim and related foundation arguments cite it whenever a dimensionless mismatch between mass and energy scales must be scored. The body is a one-line abbreviation of the unique J-cost functional.
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 module proves structural $D=3$ from eight-tick closure: period $8=2^3$ forces exactly three binary recursions, the unique dimension in which the recognition lattice is minimal and self-similar.
The cost functional is the RS J-cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the unique cost forced by the Recognition Composition Law, nonnegative for $x>0$, and strictly positive when the ratio is not one. Domain cost simply feeds the mass-to-energy ratio into that functional, converting a dimensional pair into a dimensionless recognition penalty.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No lemmas or tactics; the meaning is inherited entirely from the J-cost definition used across Cost, Gravity, Cosmology, and Spiral modules.
why it matters
Gives ConfigDim_D3_v3 a named handle for scoring mass–energy mismatch under the same J that appears in the forcing chain (T5 J-uniqueness) and the Recognition Composition Law. Sibling lemmas in the module (domainCost_at_eq, domainCost_nonneg, threshold positivity, and the ConfigDimD3 certificate) build on this abbreviation. It ties the D=3 structural theorem to the cost language used elsewhere in the monolith without introducing a new functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.