domainCost_at_eq
plain-language theorem explainer
For any nonzero real r, the domain cost of the pair (r,r) is exactly zero. Normalization lemmas for the J-cost on ratio space cite this diagonal vanishing. The proof is a one-line wrapper: unfold the domain cost, cancel the ratio to 1, and apply the unit-zero fact for J.
Claim. For every real number $r \neq 0$, the domain cost of equal arguments vanishes: the cost of the self-ratio $r/r$ under $J$ equals $0$.
background
The ambient module closes the T0–T8 forcing chain as a structural theorem (no sorry, no axioms): uniqueness of the cost $J$, the Recognition Composition Law, forced $\varphi$, the eight-tick period, $D=3$, and the derived constants. The cost is the standard RS functional $J(x)=(x-1)^2/(2x)$, equivalently $\cosh(\log x)-1$ on positives.
Domain cost is the local comparison of two nonzero reals by feeding their ratio into $J$. On the diagonal the ratio is identically 1, so the claim is the specialization of the unit identity for $J$. Upstream, Jcost_unit0 records exactly $J(1)=0$ by direct simplification of the squared-ratio formula.
proof idea
One-line wrapper. Unfold the definition of domain cost (ratio into $J$), rewrite $r/r=1$ via div_self using $r\neq 0$, then finish by the upstream lemma $J(1)=0$.
why it matters
Diagonal vanishing is the baseline sanity check that domain cost is a genuine defect: zero self-distance before nonnegativity and threshold lemmas in the same file. The module’s certificate (ForcingChainComp3Cert) packages T0–T8 completeness from $J$; this fact anchors the cost side of that package even though no downstream edge is recorded yet. It sits under the primer landmarks T5 (J-uniqueness) and the RCL, where $J(1)=0$ is the neutral element of the composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.