domainCost_at_eq
plain-language theorem explainer
When both domain arguments equal a common nonzero real r, the domain cost is exactly zero. Cosmology and ladder-normalization arguments that reduce ratios to the unit point cite this diagonal identity. The proof is a one-line unfold of the cost, rewrite of r/r to 1, and appeal to the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the J-cost of the ratio $r/r$ equals $0$.
background
The module records structural theorems for a stochastic gravitational-wave background (SGWB) built on the Recognition Science phi-ladder. Status is fully proved (zero sorry, zero axioms). The RS sketch writes $\Omega_{\mathrm{GW}} = J(\varphi)^2 \Omega_{\mathrm{matter}} \approx 0.0044$, while nHz PTA bands sit near $10^{-9}$; the file therefore isolates algebraic identities rather than a numerical fit.
Domain cost is the J-cost of the ratio of its two real arguments. The J-cost is the unique nonnegative cost forced by the Recognition Composition Law, with closed form $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_unit0 states the calibration root $J(1)=0$.
proof idea
One-line wrapper. Unfold the definition of domain cost (J applied to the ratio of the two arguments). Rewrite that ratio via div_self under the hypothesis $r\neq 0$, obtaining $J(1)$. Finish by the upstream lemma that $J(1)=0$.
why it matters
Supplies the diagonal normalization used by the module's nonnegativity and threshold lemmas (domainCost_nonneg, canonicalThreshold) and by the SGWB certificate scaffolding (SGWB3Cert, cert). In the forcing chain this is the unit root of the T5 J-cost: every equal-scale comparison is free, so only off-diagonal ladder ratios carry cost into the GW amplitude. No downstream edges are recorded yet; the lemma is local infrastructure for the structural SGWB claim that the phi-ladder amplitude sits orders of magnitude above the nHz band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.