domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the recognition J-cost of that ratio: J(m/e). Gravity and GW-memory arguments in this module cite it as the local cost of a strain or energy-scale mismatch. The body is a one-line alias of the forced cost functional J(x)=(x+x^{-1})/2-1.
Claim. For real $m$ and $e$, the domain cost is $\mathrm{domainCost}(m,e) := J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
Recognition Science forces a unique nonnegative 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$), fixed already at forcing step T5. Several modules re-export the same $J$ under the name Jcost; upstream docs call it "the RS recognition cost of a positive ratio" and note it is strictly positive off the identity ratio.
This module treats gravitational-wave memory as a J-cost fraction of peak strain: structurally $\delta h = J(\varphi),h_{\mathrm{peak}}$, with $J(\varphi)\approx 11.8%$ sitting inside the empirical 5–15% memory band. Domain cost packages the same $J$ applied to a mass-over-energy (or analogous scale) ratio, so later lemmas can talk about cost of a domain mismatch without repeating the formula.
proof idea
Pure definitional abbreviation: the right-hand side is the standard J-cost of the quotient $m/e$. No lemmas, tactics, or hypotheses; downstream results unfold or rewrite with this alias.
why it matters
Gives the module a named handle for "cost of a mass/energy (or strain-scale) ratio" before proving nonnegativity, evaluation identities, and the GW-memory certificate. The module status is a structural theorem (0 sorry, 0 axiom) asserting that canonical GW memory is the J-cost of $\varphi$ times peak strain, consistent with the empirical memory fraction. That sits on the forced J from T5 and the golden ratio $\varphi$ from T6. Sibling facts (nonnegativity, evaluation at equality, canonical threshold, and the inhabited GWMemory3Cert) build directly on this alias even though the dependency graph lists no external used_by edges yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.