domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e) with the standard RS cost J(x)=(x+x^{-1})/2-1. Cosmology and SGWB arguments cite it when a mass scale is compared to an energy scale on the phi-ladder. The body is a one-line abbreviation of Jcost.
Claim. For real $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 module treats the stochastic gravitational wave background (SGWB) as a structural RS claim: $\Omega_{\mathrm{GW}}=J(\varphi)^2\Omega_{\mathrm{matter}}$ at the phi-ladder level, with a much smaller nHz band value than the naive product. Status is structural (no sorry, no axiom).
The only primitive used here is the J-cost. Upstream definitions fix $J(x)=\frac{1}{2}(x+x^{-1})-1$, the unique cost forced by the Recognition Composition Law (T5). Doc-comments call it the RS recognition cost of a positive ratio, strictly positive when the ratio is not one, and non-negative for $x>0$.
Domain cost simply specializes that functional to the dimensionless ratio of a mass parameter to an energy parameter, the natural comparison scale in the SGWB and related cosmology bridges.
proof idea
Pure definition: expand as $J(m/e)$ by applying the shared Jcost abbreviation. No tactics, no lemmas, no side conditions in the body.
why it matters
Gives the local cost scale for mass-versus-energy comparisons inside the SGWB-from-phi-ladder development (Plan v7, 117th pass). Sibling facts (domainCost_at_eq, domainCost_nonneg) and the certificate bundle (SGWB3Cert, cert) sit on top of this abbreviation; the module claims a structural match $\Omega_{\mathrm{GW}}\sim 10^{-9}$ at nHz against the RS product $J(\varphi)^2\Omega_m$.
Framework landmarks: J is the T5 unique cost from the RCL; $\varphi$ enters the SGWB amplitude via $J(\varphi)$. No downstream edges are recorded yet, so the definition is infrastructure for the certificate rather than a cited lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.