domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost J to the ratio of a mass scale m to an energy scale e. Cosmology and gravity arguments that need a dimensionless mismatch between mass and energy cite this wrapper. The body is a one-line abbreviation of the unique RS cost functional on 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 recognition cost of a positive ratio.
background
Recognition Science measures mismatch of positive ratios by the J-cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all fix this same functional; EnergyProcessingBridge records that it is the unique cost forced by the Recognition Composition Law. $J(1)=0$ and $J(x)>0$ for $x\neq 1$ (when $x>0$).
This module is Cosmology RS Structural Module 9 in the forcing chain T5 (J-uniqueness) through T8 ($D=3$). Domain cost specializes J to a mass-over-energy ratio, the natural dimensionless input when comparing a mass scale to an energy (or temperature) scale in cosmological structure arguments.
proof idea
Pure definition: domainCost m e is defined to be Jcost (m / e). No proof obligations; the mathematical content is entirely that of J on the quotient.
why it matters
Gives the module a named mass-energy cost so later structural facts (nonnegativity, evaluation identities, canonical thresholds, and the RSCOSStructural009 certificate among the siblings) can speak in domain language rather than raw J. Sits on the T5 landmark: once J is forced unique by the composition law, every cosmological cost of a ratio is this same functional. No downstream used_by edges are recorded yet; the definition is local scaffolding for the structural certificate in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.