domainCost_at_eq
plain-language theorem explainer
Equal nonzero domain scales incur zero domain cost: the cost of matching a scale against itself vanishes. Anyone normalizing Recognition Science cost functionals, or checking the top-Yukawa unit-coupling baseline, would cite this. 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)$ is zero. Equivalently, feeding the self-ratio $r/r=1$ into the RS cost $J$ yields $J(1)=0$.
background
Physics RS Module 7 treats the top Yukawa as fixed at unity at unification: the top quark sits on the $\phi^0=1$ coupling rung. Status is structural (no sorry, no axiom).
The underlying cost is the unique RS functional $J$, written $J(x)=(x-1)^2/(2x)$ (equivalently $\cosh(\log x)-1$). Its unit normalization is the upstream lemma $J(1)=0$. Domain cost compares two real scales by evaluating $J$ on their ratio; the present statement is the diagonal case of that comparison.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite the ratio by division-by-self (using $r\neq 0$) to obtain $J(1)=0$. Discharge with the upstream lemma that $J(1)=0$.
why it matters
Fixes the zero of domain cost on equal scales, the normalization baseline for Module 7's claim that the top Yukawa is the unit coupling $y_t=1$ at unification. Sibling results in the same module (nonnegativity of domain cost, the canonical threshold, and the Module-7 certificate) sit on this diagonal vanishing. No external downstream users are recorded yet; the lemma is local infrastructure for the top-Yukawa structural theorem rather than a forcing-chain step (T5--T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.