domainCost_at_eq
plain-language theorem explainer
On the positive reals the domain cost vanishes on the diagonal: evaluating it at equal nonzero arguments yields zero. Cosmology and cost-geometry arguments cite this to normalize thresholds and certify that identical scale ratios carry no excess cost. The proof unfolds the cost, cancels the ratio to 1, and applies the unit identity for J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero: $C_{\mathrm{dom}}(r,r)=0$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. The unit identity states $J(1)=0$: perfect scale match carries zero cost.
In this cosmology module the domain cost of a pair of scales is the J-cost of their ratio. The module targets a structural certificate for the dimensionless combination $\Lambda\ell_P^2$, reported in RS units as $8\varphi^5/45$ inside $(1.88,2.03)\times 10^{-122}$, consistent with the Planck value near $1.99\times 10^{-122}$.
The present lemma is the diagonal normalization of that cost: when the two arguments coincide and are nonzero, the ratio is 1 and the cost collapses.
proof idea
One-line wrapper. Unfold the definition of domain cost (J of the ratio). Rewrite the ratio $r/r$ to $1$ by div_self using $r\neq 0$. Finish with the upstream lemma Jcost_unit0, which states $J(1)=0$.
why it matters
Diagonal vanishing is the baseline that lets later cosmology certificates treat excess cost as a pure off-diagonal defect. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and sits in the RS cosmology stack that pins $\Lambda\ell_P^2$ to the $\varphi$-ladder band. No downstream dependents are recorded yet; siblings such as nonnegativity of domain cost and the canonical threshold build on the same cost primitive. The result is local bookkeeping rather than a forcing-chain step (T5–T8), but it keeps the cost geometry consistent with the Recognition Composition Law normalization $J(1)=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.