domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e) with the standard RS J-functional. Cosmology proofs that compare mass and energy scales against a threshold cite it as the local cost measure. The body is a one-line abbreviation of Jcost on the quotient.
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$, also written $\cosh(\log x)-1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse) all fix this same functional: cost vanishes only at ratio one and is nonnegative for $x>0$.
This file is Cosmology RS Module 1. The module doc targets a structural match for $\Omega_\Lambda$: $11/16-\alpha/\pi=0.685$ against Planck $0.685$ at $0.665\sigma$, status STRUCTURAL THEOREM (zero sorry, zero axiom). Domain cost is the local cost primitive used when mass and energy scales enter that comparison.
proof idea
Pure definition: apply the shared J-cost to the quotient $m/e$. No lemmas, no tactics; the body is the abbreviation Jcost (m / e).
why it matters
Gives the cosmology module a named cost on mass-versus-energy ratios so later facts (nonnegativity, evaluation at equality, canonical thresholds, and the RSCosmo001 certificate) can speak in RS units rather than raw quotients. It sits under the T5 J-uniqueness landmark: the same $J$ forced by the Recognition Composition Law is reused here for cosmological scale comparison, tying $\Omega_\Lambda$ bookkeeping to the forcing chain rather than an ad hoc penalty. No downstream edges are recorded yet; siblings in-module are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.