domainCost_at_eq
plain-language theorem explainer
Equal nonzero scales incur zero domain cost: the J-cost of a scale matched to itself vanishes. Cosmology arguments that need a zero baseline on the diagonal of the cost cite this identity. The proof is a one-line unfold reducing the ratio to 1 and applying J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of the matched pair $(r,r)$ is zero.
background
Recognition Science measures multiplicative scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law. It vanishes only at unit ratio: $J(1)=0$.
This module is Cosmology RS Structural 4, recording the gap-45 identity $D^2(D+2)=9\cdot 5=45$ as the minimum rung for stable self-reference at $D=3$. Domain cost is the local pairing of two real scales through $J$ of their ratio; the present claim is the diagonal fixed-point of that pairing.
The sole upstream fact is the unit lemma: $J(1)=0$, obtained by direct simplification of the closed form of $J$.
proof idea
One-line wrapper. Unfold domain cost so the goal becomes $J(r/r)=0$. Rewrite $r/r=1$ from the hypothesis $r\neq 0$, then apply the unit lemma $J(1)=0$.
why it matters
Local structural support for the gap-45 certificate in this module (minimum self-reference rung at three spatial dimensions). Siblings such as nonnegativity of domain cost and the canonical threshold sit on the same cost; a zero diagonal is the baseline those comparisons need.
No external downstream edges are recorded yet. Framework landmarks in view are T5 (J-uniqueness) and T8 ($D=3$). The claim does not itself prove gap-45; it only clears the cost identity used when matching a scale to itself inside that structural stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.