domainCost_at_eq
plain-language theorem explainer
Equal nonzero scales carry zero domain cost: the J-cost of the ratio r/r is identically zero. Cited by anyone normalizing the RS cost before linking it to Solomonoff-style algorithmic probability. Proof is a one-line unfold of the ratio definition, rewrite to 1, and the unit root of J.
Claim. For every real $r \neq 0$, the domain cost at equal arguments vanishes: if $C(x,y) := J(x/y)$ with $J$ the Recognition cost, then $C(r,r) = 0$.
background
The module connects Recognition Science J-cost to Solomonoff algorithmic probability. Module status is structural (zero sorry, zero axiom): at an RS-optimal encoding the shortest program length scales as $J(\varphi)\cdot|x|$, so the universal prior peaks at the $J(\varphi)$ compression rate.
The cost $J$ is the unique functional forced by the Recognition Composition Law. In closed form $J(x)=(x-1)^2/(2x)$, equivalently $(x+x^{-1})/2-1$, and the unit lemma records $J(1)=0$. Domain cost pulls $J$ back along the ratio of two nonzero reals, measuring scale mismatch. The present identity is the diagonal normalization of that pullback.
proof idea
One-line wrapper. Unfold domain cost to expose $J(r/r)$. Rewrite the ratio via div_self using $r\neq 0$, obtaining $J(1)$. Finish by the upstream lemma Jcost_unit0, which states $J(1)=0$ by direct simplification of the closed form of $J$.
why it matters
Structural normalization inside the Algorithmic Probability from J-Cost development. Equal scales must cost zero before any compression-rate or prior comparison is meaningful; siblings (nonnegativity of domain cost, canonical threshold, the inhabited certificate) sit on that baseline. The graph currently lists no downstream dependents, so this is a local support lemma rather than a chain step. It inherits the global $J$ from the forcing chain (T5 J-uniqueness) and the Recognition Composition Law; the same unit root $J(1)=0$ that appears throughout RS cost calculus is reused here for the information-theoretic bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.