domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real against itself is zero: equal arguments incur no recognition cost. Cited when checking that the RS cost is a true defect (vanishes on the diagonal). One-line wrapper: unfold the ratio definition, cancel by div_self, and apply J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of $r$ against itself vanishes: if the domain cost of a pair is the Recognition cost $J$ of their ratio, then $J(r/r) = 0$.
background
The Recognition cost $J$ is the unique symmetric cost forced by the Recognition Composition Law. Closed forms used here are $J(x)=(x+x^{-1})/2-1$ and the squared-ratio form $J(x)=(x-1)^2/(2x)$. By construction $J(1)=0$; that unit identity is the sole upstream lemma.
In this module the domain cost of a pair of reals is the cost of their ratio. The local setting is Foundation structural module 10: once $E_{\mathrm{coh}}$ is fixed by the electron mass, all predictions are parameter-free. Status is a structural theorem package (zero sorry, zero axiom).
The upstream unit lemma states exactly $J(1)=0$, proved by simplifying the closed form of $J$.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio via division-by-self (using $r\neq 0$) to obtain $J(1)$. Finish by the upstream unit lemma $J(1)=0$.
why it matters
Zero on the diagonal is the minimal sanity check that the Recognition cost is a genuine defect measure: equal scales cost nothing. The declaration sits in Foundation structural module 10 alongside nonnegativity and the structural certificate, packaging calibration facts used after $E_{\mathrm{coh}}$ is set once by the electron mass.
No recorded downstream dependents yet. It supports the broader RS claim that predictions become parameter-free once that single calibration is fixed, and it is consistent with T5 J-uniqueness ($J(x)=\cosh(\log x)-1$) from the forcing chain. It does not itself force $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.