domainCost
plain-language theorem explainer
Defines the domain cost of a mass–energy pair as the recognition cost of their ratio: J(m/e). Cosmology proofs that compare scales against a canonical threshold cite this. It is a one-line abbreviation of the forced J-cost on the dimensionless ratio 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 forces a unique cost on positive ratios via the Recognition Composition Law. That cost is $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative for $x > 0$.
This module is Cosmology Structural 6, whose theme is RS $\phi$ uniqueness (the self-similar fixed point $\phi = 1 + 1/(1+1/(1+\cdots))$). Domain cost packages $J$ on a mass-to-energy (or analogous scale) ratio so later lemmas can compare cosmological domains to a canonical threshold without rewriting the functional each time.
Upstream, every $J\mathrm{cost}$ import is the same formula: "the RS recognition cost of a positive ratio" and "the unique cost functional forced by the Recognition Composition Law."
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No lemmas or tactics; the body is the single application of the forced J-cost to the ratio.
why it matters
Gives cosmology a named handle on scale mismatch cost inside the structural $\phi$-uniqueness module. Sibling facts (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) build nonnegativity and threshold comparisons on top of it, feeding the module certificate RSCOSStructural006Cert.
In the forcing chain this sits under T5 (J-uniqueness) and T6 ($\phi$ as self-similar fixed point): domain comparisons inherit the unique cost rather than an ad hoc metric. No downstream 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.