domainCost
plain-language theorem explainer
Domain cost assigns to a mass scale m and energy scale e the recognition cost of their ratio. Anyone working the domain-coverage milestone or threshold certificates in FinalModule_1399 cites it. The body is a one-line abbreviation of the standard J-cost 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 scales by the J-cost $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all fix this same functional: it vanishes only at ratio one and is strictly positive for any genuine distinction.
This module is the structural certificate for the domain-coverage milestone (Plan v7, 109th pass): zero sorry, zero axiom. Domain cost is the local specialization that feeds ratio $m/e$ into $J$, so later threshold and certificate objects can talk about mass-versus-energy mismatch in RS-native units without reopening the definition of $J$.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No lemmas, no tactics; the equality is by rfl wherever needed (as in the sibling domainCost_at_eq).
why it matters
Gives the milestone module a single named hook for mass/energy mismatch under the forced J-cost (T5 uniqueness: $J(x)=\frac12(x+x^{-1})-1$). Sibling objects canonicalThreshold, MilestoneCert, and cert sit on top of this cost; without a stable domain-cost symbol the certificate would re-inline $J(m/e)$ everywhere. It does not itself prove positivity or threshold bounds; those live in the neighboring lemmas. Framework role is local bookkeeping inside the domain-coverage structural theorem, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.