domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of r against itself is zero. Structural and certificate authors in the gap-45 module cite this to confirm the cost is a true defect (vanishes on the diagonal). The proof is a one-line unfold of the domain cost to J on the unit ratio, then the unit identity of J.
Claim. For every real $r \neq 0$, the domain cost of $r$ relative to itself is zero.
background
This module records structural facts around RS gap-45: at spatial dimension $D=3$ one has $D^2(D+2)=45$, the minimum rung for stable self-reference. Status is a pure structural theorem (no sorry, no axioms).
The underlying cost is the Recognition J-functional, uniquely fixed by the composition law and normalized so $J(1)=0$. Upstream, Jcost_unit0 states exactly that unit identity; equivalently $J(x)=(x-1)^2/(2x)$. The domain cost compares two nonzero reals by feeding their ratio into $J$, so self-comparison is the unit case.
Sibling facts in the same file establish nonnegativity of the domain cost and a positive canonical threshold used by the module certificate.
proof idea
One-line wrapper. Unfold the domain cost definition (ratio into $J$), rewrite $r/r=1$ by the nonzero hypothesis, and finish with the upstream unit identity $J(1)=0$.
why it matters
Diagonal vanishing is the first sanity check that the domain cost is a genuine defect measure rather than an arbitrary positive function. In the Recognition forcing chain this sits under T5 (J-uniqueness) and the $D=3$ landmark (T8), and it supports the gap-45 structural story: minimum rung for stable self-reference.
No downstream dependents are wired yet; within the module it underwrites the nonnegativity lemma and the inhabited structural certificate for RS-FDN-004. Without it, the certificate could not honestly claim a zero self-cost baseline before quoting thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.