domainCost_at_eq
plain-language theorem explainer
On the diagonal of nonzero reals the domain cost vanishes: equal arguments yield cost zero. Cited by anyone checking that the structural cost is a true defect (zero iff scales match). Proof is a one-line unfold: cancel the ratio to 1 and apply the unit identity for J.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero.
background
This module is Foundation structural item 6: uniqueness of $\varphi$ as the self-similar fixed point of the continued fraction $1+1/(1+1/(\cdots))$, recorded as a structural theorem with no sorry and no axioms.
The ambient cost is the Recognition $J$-functional (T5), written in Lean as Jcost. Upstream, Jcost_unit0 states $J(1)=0$, which is immediate from the squared-ratio form $J(x)=(x-1)^2/(2x)$ (equivalently $J(x)=\cosh(\log x)-1$). The local domainCost is the cost of a pair of real scales via their ratio: after unfolding, domainCost r s is $J(r/s)$ (for $s\neq 0$).
Thus the diagonal claim is exactly the statement that equal nonzero scales sit at the unit point of $J$.
proof idea
One-line wrapper. Unfold domainCost so the goal is $J(r/r)=0$. Rewrite $r/r=1$ by div_self using the hypothesis $r\neq 0$. Finish by exact Jcost_unit0.
why it matters
Sanity check that the structural domain cost is a genuine defect on scale pairs: it vanishes when the two arguments coincide. That is the minimal algebraic input any later comparison or threshold argument needs before talking about positive cost off the diagonal.
The parent module targets RS $\varphi$-uniqueness (T6: $\varphi$ forced as the self-similar fixed point). Sibling facts (domainCost_nonneg, canonicalThreshold_pos, and the module certificate RSFDNStructural006Cert) package nonnegativity and a positive canonical threshold around the same cost. The zero-on-diagonal lemma closes the unit case of that package and sits under the T5 $J$-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$). No downstream theorems are wired yet; the immediate consumers are the module certificate and any later forcing steps that quote a vanishing cost at matched scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.