domainCost_at_eq
plain-language theorem explainer
For any nonzero real scale r, the recognition cost of comparing r to itself is exactly zero. Cost-curve and Logo5 arguments cite this as the diagonal identity of the domain cost. The proof unfolds the cost to J of the ratio, collapses r/r to 1, and applies the unit-zero lemma for J.
Claim. For every real number $r\neq 0$, the recognition domain cost of $r$ against itself vanishes: if the cost is $J$ of the ratio of the two arguments, then $J(r/r)=0$.
background
The Logo5 module treats the RS cost curve as the structural signature of Recognition Science: $J(x)=(x+1/x)/2-1$ on $(0,\infty)$, with unique minimum $J(1)=0$ and the value $J(\varphi)$ at the golden ratio. In RS-native language this is the T5 J-cost (equivalently $\cosh(\log x)-1$, or the squared-ratio form $(x-1)^2/(2x)$).
Domain cost is that same $J$ evaluated on a ratio of two real scales. The only upstream fact needed here is the unit identity: $J(1)=0$, recorded as the lemma that simplifies $J$ at the multiplicative unit. The nonzero hypothesis on $r$ is exactly what makes the ratio $r/r$ well-defined and equal to 1.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite the ratio to 1 by the field identity $r/r=1$ under $r\neq 0$, then close with the upstream unit-zero lemma $J(1)=0$.
why it matters
Anchors the diagonal vanishing of the RS logo curve: self-comparison costs nothing, which is the geometric content of the unique minimum of $J$ at the unit ratio. In the forcing chain this is the local identity side of T5 J-uniqueness. Inside the module it sits beside nonnegativity and the canonical threshold siblings that turn the same curve into a certified Logo5 package (0 sorry, 0 axiom). No external used-by edges are recorded yet; the lemma is infrastructure for any later argument that normalizes a ratio to the identity before quoting cost bounds or the $\varphi$-threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.