domainCost_at_eq
plain-language theorem explainer
The cost of matching any nonzero real scale to itself is exactly zero. Compression-ratio work in the RS information layer cites this as the diagonal baseline of the domain cost. Proof is a one-line unfold: the self-ratio becomes 1, and J(1)=0 finishes it.
Claim. For every real $r \neq 0$, the domain-scale cost of $r$ against itself vanishes: the cost of the ratio $r/r$ under $J$ is $0$.
background
This module treats the RS compression ratio as a structural theorem: maximum lossless compression is the Kolmogorov limit, and RS claims an achievable factor $J(\varphi)^{-1} \approx 8.47\times$ for structured data at phi-rung complexity, while random data stays at $1\times$ (incompressible).
Domain cost compares two real scales by feeding their ratio into the RS cost $J$. Here $J$ is the unique nonnegative cost forced by the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$) and normalization $J(1)=0$.
The sole upstream fact is the unit identity: $J(1)=0$, obtained by direct simplification of that closed form.
proof idea
One-line wrapper. Unfold domain cost so the goal is $J(r/r)=0$. Rewrite $r/r=1$ from the hypothesis $r\neq 0$, then apply the unit lemma $J(1)=0$.
why it matters
Fixes the zero of domain cost on the diagonal, the baseline against which any nontrivial compression ratio is measured in this module. Siblings cover nonnegativity of domain cost, the canonical positive threshold, and the inhabited CompressionRatioCert that packages the RS claim $J(\varphi)^{-1}$ on structured data. No downstream dependents are wired yet; the lemma is local scaffolding for the Information-domain compression story and sits under the structural (0 sorry, 0 axiom) status of the module. Landmark contact is T5 J-uniqueness and the phi fixed point that sets the numerical factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.