domainCost_at_eq
plain-language theorem explainer
Whenever the two scale arguments of the domain cost agree and are nonzero, the cost is exactly zero. Cost-calculus and threshold arguments in the phi-square module cite this as the on-diagonal normalization. The proof is a one-line wrapper: unfold the definition, cancel the ratio to 1, and apply the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ vanishes: the cost of matching a nonzero scale against itself is $0$.
background
The ambient module records the structural identity $\varphi^2 = \varphi + 1$ and its Fibonacci-style consequences for the recognition recursion. The cost functional $J$ is the unique nonnegative cost fixed by the Recognition Composition Law (T5); one convenient form is $J(x) = (x-1)^2/(2x)$, which vanishes at the unit $x=1$.
Domain cost is the two-argument specialization that scores a pair of nonzero real scales by feeding their ratio into $J$. The upstream lemma Jcost_unit0 states precisely $J(1)=0$, so any pair whose ratio is identically one must carry zero cost. That is the local setting for the on-diagonal identity proved here.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $J(r/r)=0$. Rewrite the ratio by div_self using the hypothesis $r\neq 0$, obtaining $J(1)=0$. Discharge by the upstream lemma that $J$ vanishes at the unit.
why it matters
Inside the phi-square identity module this is the basic normalization that the cost of a scale against itself is zero. It underwrites nonnegativity and threshold lemmas in the same file (domain-cost nonnegativity, the canonical threshold, and the certificate bundle), even though no external used-by edge is recorded yet. In the broader forcing chain it is the elementary consequence of T5 J-uniqueness that the self-similar fixed point $\varphi$ and the eight-tick ladder sit on a cost landscape whose diagonal is identically zero. No open scaffold is involved: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.