domainCost_at_eq
plain-language theorem explainer
Equal nonzero scale arguments make the domain cost vanish. Anyone verifying that the φ-ladder domain cost is a true defect (zero on the diagonal) cites this. The proof unfolds the definition to J of a ratio, reduces that ratio to 1, and applies the unit-zero lemma for J.
Claim. For every real $r \neq 0$, the domain cost of the matched pair equals zero: if the cost is $J$ of the scale ratio, then $J(r/r) = 0$.
background
The module treats string compactification radii on the φ-ladder: extra dimensions sit at $R_{\mathrm{comp}} = \ell_{\mathrm{Pl}} \varphi^{-k}$, with $k=0$ near the Planck scale and $k \approx \log(M_{\mathrm{Pl}}/M_{\mathrm{EW}})/\log\varphi \approx 106$ at the electroweak scale. Status is structural (no sorry, no axioms).
Domain cost scores mismatch between two positive scale parameters by feeding their ratio into the Recognition cost $J$. Upstream, $J$ is normalized so $J(1)=0$, equivalently $J(x)=(x-1)^2/(2x)$. The present lemma is the diagonal case of that normalization: matched scales give ratio 1 and therefore zero cost.
proof idea
One-line wrapper. Unfold the domain-cost definition (cost of the ratio of the two arguments). Rewrite $r/r=1$ by div_self using $r\neq 0$. Finish with the upstream lemma $J(1)=0$.
why it matters
Pins the defect property of domain cost on the diagonal, which any string-length certificate in this module needs before comparing compactification radii to φ-ladder rungs. Siblings cover nonnegativity, the canonical threshold, and the inhabited certificate type; this equality is the zero-locus half of that package. In the broader framework it is local bookkeeping for the φ-ladder mass/length yardstick, not a forcing-chain step (T5–T8). No downstream edges are recorded yet; the lemma exists to keep the compactification-radius story cost-clean when the two scales coincide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.