domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the cost of the ratio r/r is zero. Cited by anyone normalizing the Recognition cost on the diagonal of equal scales. Proof unfolds the definition, cancels the ratio to 1, and applies the unit root J(1)=0.
Claim. For every real $r \neq 0$, the Recognition domain cost of the pair $(r,r)$ is zero, i.e. $J(r/r)=0$ where $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$.
background
The Recognition cost is $J(x)=(x+x^{-1})/2-1$, equivalently $J(x)=(x-1)^2/(2x)$ for $x>0$. It is the unique functional forced by the Recognition Composition Law and the T5 step of the forcing chain. Its global minimum is zero and is attained at the identity ratio $x=1$.
In this summary module the domain cost of a pair of reals is the cost of their ratio: domain cost$(x,y)=J(x/y)$ whenever $y\neq 0$. The module is a structural certificate (zero sorry, zero axiom) that one equation for $J$ forces $\phi$, gap-45, $D=3$, and the derived constants.
Upstream, the unit lemma states $J(1)=0$ by direct simplification of the closed form.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio to $1$ via division-by-self using the hypothesis $r\neq 0$. Finish by the unit lemma $J(1)=0$.
why it matters
Local normalization fact inside the Recognition Science complete summary certificate (Plan v7). It records that equal scales carry zero recognition cost, the diagonal minimum of $J$. Siblings in the same module (nonnegativity of domain cost, canonical threshold positivity) sit on the same foundation. Framework landmark: T5 J-uniqueness, whose unique cost has a global zero at the identity ratio. No external dependents are wired yet; the lemma is internal scaffolding for the summary cert that packages forced $\phi$, eight-tick structure, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.