domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real against itself is zero: comparing a scale to the same scale incurs no J-cost. Anyone working the RS rung-spacing or ladder-comparison lemmas would cite this. The proof is a one-line unfold-and-rewrite that reduces to the known unit root J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself vanishes: $\mathrm{domainCost}(r,r)=0$. Equivalently, if domain cost is the J-cost of the ratio of the two arguments, then $J(r/r)=J(1)=0$.
background
Recognition Science measures scale mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. The unit root is elementary: $J(1)=0$ (lemma Jcost_unit0).
This module packages structural facts about RS rung spacing, where adjacent rungs differ by the golden ratio $\varphi$. Domain cost is the natural two-argument lift that scores how far one positive scale sits from another via $J$ of their ratio. The local setting is a pure structural theorem file: zero sorry, zero axioms.
The only upstream fact needed is that unit evaluation of $J$ is zero, which follows by direct simplification of either closed form.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$, then apply the lemma $J(1)=0$.
why it matters
Diagonal vanishing is the sanity check that any cost used for rung or scale comparison must satisfy: a rung compared to itself contributes nothing. In the RS ladder picture, mass and coupling placements sit on powers of $\varphi$; domain cost is the natural defect between two such placements. This lemma closes the zero-self-distance clause of that defect, keeping later nonnegativity and threshold arguments honest.
No downstream users are wired yet in the graph, so the result presently stands as a structural certificate inside Mathematics RS Structural Module 8 rather than a leaf of a larger forcing chain (T5–T8). It is still the right primitive for any future comparison of adjacent rungs or of a measured scale against a canonical threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.