domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the recognition cost of their ratio m/e. It is the local cost functional used when the RS string-landscape module compares vacuum structure to the string ~10^500 count. The body is a one-line composition of the forced J-cost with the quotient.
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
The Recognition Science cost functional is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the unique cost forced by the Recognition Composition Law, nonnegative for $x>0$, and strictly positive when the ratio is not one.
This module frames a structural comparison between the string landscape (~$10^{500}$ vacua) and an RS count built from powers of $\phi$. Status is structural theorem (zero sorry, zero axiom). Domain cost is the elementary cost of a mass-to-energy (or scale-to-scale) ratio inside that comparison.
Sibling lemmas immediately record evaluation at equality and nonnegativity; a canonical threshold sits nearby for landscape cutoffs.
proof idea
Pure definition: no proof obligations. The body substitutes the ratio $m/e$ into the already-defined $J$-cost. All analytic properties (nonnegativity, uniqueness under RCL, zero only at ratio one) are inherited from upstream $J$ and proved in sibling or imported lemmas, not here.
why it matters
Gives the RS-native cost of a two-scale ratio inside the string-landscape structural theorem. The module asks whether RS vacuum counting (powers of $\phi$, linked to T6 self-similarity and T8 $D=3$) can match or bound the string ~$10^{500}$ figure; domain cost is the local cost atom for that comparison. Downstream use is not yet wired in the graph (used_by empty), but siblings domainCost_nonneg, canonicalThreshold, and the landscape certificate cert sit in the same file and are the natural consumers. Ties to the forcing chain only through $J$ (T5 uniqueness) and $\phi$-powers in the module narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.