domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain arguments carry zero cost: the self-ratio sits at the unit root of J. Cosmology and rung-ladder arguments that need a vanishing baseline on the diagonal cite this identity. The proof is a one-line unfold of the domain-cost definition, rewrite of the self-ratio to 1, and the unit lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if domain cost is the J-cost of the ratio of its two arguments, then $J(r/r) = J(1) = 0$.
background
Recognition Science measures mismatch of positive scales by the J-cost $J(x)=(x+x^{-1})/2-1$, also written $(x-1)^2/(2x)$. This cost vanishes only at the unit ratio and is the unique generator forced by the Recognition Composition Law (forcing step T5).
This module is Cosmology RS Structural 8: structural facts about RS rung spacing, where adjacent rungs differ by the golden-ratio factor $\phi$. Domain cost applies $J$ to a ratio of two real arguments, so equal nonzero arguments reduce to $J(1)$.
The sole upstream fact used here is the unit root of the cost: $J(1)=0$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of the two arguments). Rewrite $r/r$ to $1$ with the hypothesis $r\neq 0$. Finish by the upstream lemma $J(1)=0$.
why it matters
Supplies the diagonal zero for domain cost inside the cosmology structural package. Sibling lemmas (nonnegativity, canonical threshold positivity) and the module certificate build on the same cost primitive; together they form a zero-sorry structural block for rung-ladder comparisons.
In the broader framework this is an elementary consequence of T5 J-uniqueness: once cost is $J$, self-comparison is free. No downstream dependents are recorded in the graph yet; the lemma is local scaffolding for any later cosmology identity that normalizes equal scale factors or equal rung coordinates to zero cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.