domainCost
plain-language theorem explainer
The domain cost of a mass-energy pair is the recognition cost of their ratio: J(m/e). Structural work on the RS gap-45 (minimum rung for stable self-reference at D=3) uses this as the local cost on the mass-to-energy scale. The definition is a one-line specialization of the unique J-cost forced by the Recognition Composition Law.
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 fixes 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$, and is forced already at T5 of the unified forcing chain. It vanishes only at ratio one and is nonnegative for $x > 0$.
This module is the structural mathematics package for RS gap-45: at spatial dimension $D = 3$ one has $D^2(D+2) = 45$, identified as the minimum rung for stable self-reference. The local objects are real mass and energy scales $m,e$, and the natural dimensionless probe is their ratio $m/e$.
Upstream, every copy of Jcost in the monolith is the same functional: "the RS recognition cost of a positive ratio" and "the unique cost functional forced by the Recognition Composition Law." Domain cost simply feeds the mass-energy ratio into that functional.
proof idea
Pure definitional abbreviation: apply the global J-cost to the single real argument $m/e$. No lemmas, no tactics, no side conditions at the definition site. Nonnegativity and evaluation identities appear in sibling lemmas once positivity of the ratio is assumed.
why it matters
Gap-45 is the structural claim that $D=3$ forces a minimum self-reference rung of 45. Domain cost supplies the cost language in which mass and energy scales are compared inside that package: any deviation of $m/e$ from unity incurs a positive J-cost, matching the T5 uniqueness of $J$ and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
Sibling facts (evaluation at equal arguments, nonnegativity, a canonical positive threshold, and the module certificate) sit on top of this definition. No downstream consumers are wired yet in the graph; the definition is infrastructure for the gap-45 structural theorem rather than a leaf result in the physics chain (mass ladder, alpha band, eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.