domainCost_at_eq
plain-language theorem explainer
Equal nonzero arguments make the domain cost vanish: the J-cost of the ratio r/r is zero. Cited by anyone comparing rung or scale pairs under the Recognition cost. One-line wrapper: unfold the ratio definition, cancel r/r to 1, apply J(1)=0.
Claim. For every real $r\neq 0$, the domain cost of the pair $(r,r)$ is zero. Equivalently, if domain cost is the Recognition cost $J$ of the ratio of its arguments, then $J(r/r)=J(1)=0$.
background
Recognition Science measures mismatch of positive scales by the cost $J$, forced unique by the Recognition Composition Law (T5). Two common writings are $J(x)=(x+x^{-1})/2-1$ and $J(x)=(x-1)^2/(2x)$; both give $J(1)=0$ and $J(x)\ge 0$.
This module is Foundation structural module 8 on RS rung spacing: adjacent rungs differ by the golden factor $\varphi$. Domain cost of a pair of scales is the $J$-cost of their ratio, so equal scales are the zero-cost baseline.
Upstream, the lemma $J(1)=0$ is proved by direct simplification of the closed form of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (ratio form), rewrite $r/r=1$ from the hypothesis $r\neq 0$, then apply the upstream unit lemma $J(1)=0$.
why it matters
Gives the identity baseline for cost comparisons on the $\varphi$-ladder: equal rung positions carry zero domain cost. Lives in the structural rung-spacing module (adjacent factors $\varphi$), which is status-clean (0 sorry, 0 axiom). Sibling facts in the same file (nonnegativity of domain cost, positivity of the canonical threshold, and the structural certificate) rest on this zero-at-equality fact. Framework landmark: T5 J-uniqueness calibrates the cost so the unit ratio is exactly the zero locus; this lemma is that calibration at equal arguments. No downstream dependents are recorded yet in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.