domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the domain cost of comparing r to itself is exactly zero. Cosmology proofs that normalize ratios or check fixed points of the ISM dust-fraction certificate cite this diagonal vanishing. The argument unfolds the cost definition, reduces the self-ratio to 1, and applies J(1)=0.
Claim. For every real number $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the cost of the self-ratio equals $0$.
background
Module RS_Cosmo_Module_011 treats the ISM dust fraction as a structural match: $J(\varphi)^2 \approx 1.39%$ against the empirical $\sim 1%$ band, with status STRUCTURAL THEOREM (zero sorry, zero axiom).
The underlying cost is the Recognition Science J-functional $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$. It is normalized so that the unit ratio carries zero cost. The local domain cost is the J-cost of a ratio of two nonzero real scales; on the diagonal that ratio is identically 1.
Upstream, Jcost_unit0 records the normalization $J(1)=0$ by direct simplification of the closed form.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the self-division to $1$ via div_self (using $r\neq 0$), then apply the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline sanity check for any ratio-based cost used in the cosmology certificates of this module (siblings include nonnegativity of domain cost, the canonical threshold, and the inhabited RSCosmo011 certificate). It sits under the T5 J-uniqueness landmark: once $J$ is forced, $J(1)=0$ is immediate and propagates to every self-comparison of scales. No downstream dependents are wired yet; the lemma is infrastructure for the ISM dust-fraction match rather than a parent theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.