domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Anyone building the RS AdS/CFT structural layer uses it as the bulk/boundary cost measure on real parameters. The body is a one-line abbreviation: apply the forced J-cost to m/e.
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
The ambient module treats AdS/CFT as natural in Recognition Science once spatial dimension is forced to $D=3$: bulk AdS dimension is $D+1=4$ and the CFT lives in dimension $D=3$. Status is structural (no sorry, no axiom).
The cost functional is the unique $J$ forced by the Recognition Composition Law: $J(x)=\frac{1}{2}(x+x^{-1})-1$ for $x>0$. Upstream docs phrase it as “the RS recognition cost of a positive ratio” and note that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply feeds the mass-to-energy ratio into that functional.
Sibling material in the same file develops nonnegativity, evaluation identities, and a canonical positive threshold built from this cost, so the definition is the shared primitive for those lemmas.
proof idea
Pure definition, not a proved statement. The body is the abbreviation Jcost (m / e): no tactics, no lemmas, no case splits. All analytic content (nonnegativity, zeros, thresholds) is deferred to sibling theorems that unfold this def.
why it matters
In the RS AdS/CFT story the forced $D=3$ (forcing chain T8) makes bulk dimension four automatic; domain cost is the local cost primitive that measures how far a mass–energy pair sits from the unit-ratio fixed point of $J$. That is the same $J$ fixed at T5 by the Recognition Composition Law, so the definition sits on the main uniqueness spine rather than an ad hoc bulk action.
No downstream theorems are wired yet in the graph (used_by empty). The immediate consumers are the in-module siblings: equality-at-evaluation, nonnegativity, the canonical threshold and its positivity, and the RS–AdS/CFT certificate bundle. Those close the structural claim that AdS/CFT is the natural holographic packaging of RS once $D=3$ is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.