domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science J-cost to a positive ratio m/e of two real parameters. Cosmology proofs in the reionization module cite it as the local cost of a mass-to-energy (or scale) mismatch. The declaration is a one-line definition wrapping the standard J functional on that ratio.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (for $x\neq 0$).
background
Recognition Science measures mismatch by the J-cost $J(x)=\frac{1}{2}(x+x^{-1})-1$. Upstream, this is the unique cost forced by the Recognition Composition Law and the T5 uniqueness step: it vanishes only at ratio one and is nonnegative for positive arguments.
This module is Cosmology RS Module 8 (reionization). The module doc places the structural claim that the $\phi^4$–$\phi^5$ window $6.85$–$11.09$ matches observed reionization redshifts $z_{\mathrm{reion}}\sim 7$–$10$, with zero sorry and zero axioms.
Here $m$ and $e$ are generic real parameters; the cost of their ratio is the primitive used by later nonnegativity and threshold lemmas in the same file.
proof idea
Pure definition: no proof obligations. The body applies the imported J-cost functional to the quotient $m/e$. Equivalent copies of Jcost live in Cost, RefineTrigger, and CoherenceCollapse; all are the same algebraic expression.
why it matters
Gives the reionization module a named cost on domain ratios so later certificates can talk about thresholds without reopening the J definition. Sibling results (nonnegativity of domain cost, equality at matched scales, canonical threshold positivity, and the RSCosmo008 certificate) sit on top of this abbreviation.
In the broader framework it is the local instance of T5 J-uniqueness inside cosmology: cost is always $J$ of a positive ratio. The module ties that cost language to the $\phi$-ladder window $\phi^4$ to $\phi^5$ used for reionization matching. No downstream edges are recorded yet; the declaration is infrastructure for the structural certificate in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.