domainCost
plain-language theorem explainer
Domain cost assigns to a mass m and energy scale e the recognition cost of their ratio m/e. Cosmologists and RS calibrators cite it when E_coh is fixed once by the electron mass and all later predictions must stay parameter-free. The body is a one-line abbreviation of the unique J-cost on the positive ratio.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
Recognition Science forces a unique nonnegative cost on positive ratios: $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $\cosh(\log x)-1$. Upstream modules record that this $J$ is the unique functional satisfying the Recognition Composition Law, and that $J(x)>0$ whenever $x\neq 1$.
The present module is Cosmology RS Structural Module 10. Its standing convention is that the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which every cosmological prediction is parameter-free. Domain cost is the local shorthand that feeds mass and energy scales into that $J$-cost.
proof idea
Pure definitional abbreviation: apply the already-defined $J$-cost to the ratio $m/e$. No lemmas, no tactics, no proof obligations.
why it matters
Inside the structural cosmology stack this is the primitive that turns a mass–energy pair into a dimensionless recognition cost. Sibling lemmas immediately record evaluation identities and nonnegativity; the certificate RSCOSStructural010Cert packages the module as a zero-sorry structural theorem. The construction sits under the T5 J-uniqueness landmark and the global calibration rule that $E_{\mathrm{coh}}$ is set once by the electron mass, keeping later cosmological claims free of free parameters. No downstream consumers are wired yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.