domainCost
plain-language theorem explainer
Domain cost assigns to a mass scale m and an energy (or reference) scale e the recognition cost of their ratio. Anyone working the domain-coverage milestone or threshold certificates in FinalModule_1400 will cite it. The body is a one-line abbreviation: apply the standard J-cost to m/e.
Claim. For real numbers $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) = \frac{x + x^{-1}}{2} - 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.
FinalModule_1400 is a structural milestone certificate (Plan v7, 109th pass) for domain coverage. It packages cost-of-ratio language so later threshold and certificate objects can talk about when a mass sits inside or outside a reference energy band without reopening the definition of $J$.
The two arguments are ordinary reals; positivity and non-degeneracy of the ratio are left to callers (siblings such as domainCost_at_eq and canonicalThreshold).
proof idea
Pure definitional abbreviation. The body is the single application Jcost (m / e); no tactics, no lemmas, no unfolding beyond the shared J-cost def.
why it matters
Gives the milestone module a named handle for "how expensive is this mass relative to this energy scale" in RS-native units. Downstream siblings in the same file (domainCost_at_eq, canonicalThreshold, MilestoneCert, cert) build equality and positivity facts and the inhabited certificate on top of this abbreviation.
Framework landmark: T5 J-uniqueness forces exactly this $J$, so domain cost inherits the Recognition Composition Law and the non-negativity story without local re-proof. The module claims a structural theorem with zero sorry and zero axiom; this def is the cost primitive that claim rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.