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. Information and compression workers in the RS cost calculus cite this as the zero-defect baseline when both source and code sit at the same scale. The proof is a one-line unfold-and-rewrite that reduces to the unit root of J-cost.
Claim. For every real $r \neq 0$, the domain cost of the pair $(r,r)$ is zero, i.e. $J(r/r) = 0$.
background
The ambient module fixes a structural claim about data compression rates derived from the Recognition Science J-cost: an RS-optimal code carries entropy $H$ plus a $J(\varphi)$ overhead per symbol. Domain cost is the local cost functional on a pair of positive scales, realized as $J$ of their ratio (imported from the Cost layer).
Upstream, $J$ is normalized so that $J(1) = 0$ (lemma Jcost_unit0), which is the algebraic content of the unit fixed point of the cost. The same $J$ is the unique continuous solution forced by the Recognition Composition Law and the T5 uniqueness step in the forcing chain. Here the only local need is that unit root: when the two domain arguments coincide and are nonzero, the ratio collapses to 1 and the cost must vanish.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r) = 0$), rewrite $r/r = 1$ by div_self using the hypothesis $r \neq 0$, then close by the upstream lemma $J(1) = 0$.
why it matters
Gives the zero baseline for the domain-cost functional used throughout the compression module: equal scales carry no J-overhead. That baseline is what lets the module state an RS-optimal code length of $H + J(\varphi)$ bits per symbol (about $1.118$ at $H = 1$). It sits under the T5 J-uniqueness landmark and the Recognition Composition Law, both of which force $J(1) = 0$ as the unique continuous cost root. No downstream theorems currently depend on it in the graph, but sibling facts (nonnegativity, the canonical threshold, and the DataCompr3DeepCert certificate) treat this vanishing as the reference point for positive overhead away from the diagonal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.