domainCost
plain-language theorem explainer
Defines the domain recognition cost of a mass-to-energy ratio as the standard RS J-cost of m/e. Cosmology and gravity arguments cite it whenever a positive scale ratio must be scored by the unique cost forced by the Recognition Composition Law. The body is a one-line abbreviation of Jcost.
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 Science cost of a positive ratio.
background
Recognition Science scores positive ratios by the J-cost $J(x) = \frac{1}{2}(x + x^{-1}) - 1$, equivalently $\cosh(\log x) - 1$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge, SpiralField) all expose the same functional; EnergyProcessingBridge records that it is the unique cost forced by the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ (forcing chain T5).
This module is Cosmology RS Structural Module 2. Its local setting is the golden-ratio minimum of J: $J(\varphi)=\varphi-3/2\approx 0.11803$, treated as the structural recognition cost of the self-similar fixed point $\varphi$ (T6). Domain cost simply specializes J to a mass-over-energy (or more generally scale-over-scale) ratio before nonnegativity and threshold lemmas are stated.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No tactics, no lemmas, no proof obligations. Downstream equalities such as evaluation at equal arguments reduce by unfolding this def and applying algebraic identities for J.
why it matters
Gives cosmology a named handle for the RS cost of a domain ratio (mass vs energy scale) without re-inlining J everywhere. Sibling facts in the same module (domainCost_at_eq, domainCost_nonneg, canonicalThreshold) build the structural certificate RSCOSStructural002Cert around the golden-ratio cost floor $J(\varphi)=\varphi-3/2$. That floor is the T5/T6 landmark: unique J from RCL, unique self-similar fixed point $\varphi$. No downstream users are recorded yet; the def is infrastructure for the module's own nonnegativity and threshold chain rather than a cross-module export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.