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. Citation target for anyone building the RS data-compression certificate or proving nonnegativity and threshold facts around encoding overhead. Proof is a one-line unfold that rewrites the ratio to 1 and applies J(1)=0.
Claim. For every real $r \neq 0$, the domain cost at equal arguments is zero: if $C(x,y) := J(x/y)$ with $J$ the Recognition cost $J(t)=(t+t^{-1})/2-1$, then $C(r,r)=0$.
background
The module develops optimal data compression from the Recognition J-cost. Status is structural (no sorry, no axioms). The RS claim is that optimal RS encoding carries $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy, contrasting Huffman’s $H(X)$ to $H(X)+1$ average length.
Domain cost is the bivariate lift of $J$: on a pair of nonzero reals it evaluates $J$ at their ratio. The scalar $J$ is the unique cost forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, with the squared-ratio form $J(x)=(x-1)^2/(2x)$.
Upstream, Jcost_unit0 records the normalization $J(1)=0$, which is the fixed point of self-similarity and the zero of the cost at perfect match.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes $J(r/r)=0$), rewrite the ratio by div_self using $r\neq 0$ to obtain $J(1)=0$, and close by the upstream lemma Jcost_unit0.
why it matters
Supplies the zero-self-distance identity for the domain cost used throughout the Information/DataCompression3 development. Sibling facts (nonnegativity of domain cost, positivity of the canonical threshold, and the DataCompr3Cert bundle) rest on this normalization: without $C(r,r)=0$ the overhead interpretation of $J$ would not sit at Shannon’s baseline when the symbol matches the code model.
In the forcing chain this is the local instance of T5 J-uniqueness at the unit: cost vanishes exactly on perfect recognition. It does not itself force $\varphi$ or the eight-tick structure, but it is the algebraic seed those later compression bounds need when they measure excess length in J-units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.