domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real scale, the cost is exactly zero. Domain-coverage and milestone-certificate arguments in the physics layer cite this diagonal identity as the zero-defect baseline. The proof is a one-line unfold that reduces the ratio to 1 and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals zero: feeding the ratio $r/r$ into the Recognition cost $J$ yields $J(1)=0$.
background
The Recognition cost is the unique functional $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$, forced by the Recognition Composition Law and T5 uniqueness. It vanishes if and only if its argument is the multiplicative unit 1.
Domain cost of a pair of real scales is the J-cost of their ratio. On the diagonal this ratio is identically 1 whenever the common scale is nonzero, so the cost must vanish. The local module is FinalModule_1400, a structural (zero-sorry, zero-axiom) certificate for a domain-coverage milestone in the physics layer.
Upstream, the lemma Jcost_unit0 records $J(1)=0$ by direct simplification of the definition of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is a statement about $J(r/r)$. Rewrite $r/r=1$ by the standard division identity (using the hypothesis $r\neq 0$). Finish by applying the upstream lemma that $J(1)=0$.
why it matters
Supplies the zero-defect diagonal for domain-coverage bookkeeping inside FinalModule_1400 (Plan v7, 109th pass). Any later threshold, certificate, or coverage claim in the same module can discharge the equal-scale case by citing this identity. It sits on the T5 J-uniqueness landmark: the cost that is forced to vanish only at unity. The dependency graph currently lists no external consumers; the lemma is local scaffolding for the module's MilestoneCert and related positivity facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.