domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain recognition cost vanish. Anyone normalizing ratio costs or checking J-cost fixed points at the unit would cite this. The proof is a one-line unfold: the ratio collapses to 1 and J(1)=0 finishes it.
Claim. For every real $r \neq 0$, the domain recognition cost of the pair $(r,r)$ is zero: $C_{\mathrm{dom}}(r,r)=0$.
background
Module RS_MTH_Structural_007 records the ratio symmetry of the Recognition Science J-cost: $J(x)=J(1/x)$. The domain cost is the cost of a ratio of two nonzero reals, obtained by feeding that ratio into $J$.
The underlying cost is the unique J forced by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). Upstream, $J(1)=0$ is already recorded as a one-line simplification of that definition.
Locally this lemma is the diagonal normalization: when numerator and denominator coincide, the ratio is the multiplicative unit and the cost must sit at its global minimum zero.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal is $J(r/r)=0$. Rewrite $r/r$ to $1$ by the nonzero hypothesis, then apply the upstream lemma $J(1)=0$.
why it matters
This is a structural normalization inside the J-cost symmetry package (module status: structural theorem, zero sorry). It anchors the claim that recognition cost is a pure ratio functional: identical scales carry zero cost, matching the fixed point of T5 J-uniqueness and the RCL identity at the unit.
No downstream consumers are wired yet in the graph; siblings cover nonnegativity, the canonical threshold, and the module certificate. The lemma is the base case any later comparison or threshold argument will need when both legs of a ratio sit on the same rung of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.