domainCost_at_eq
plain-language theorem explainer
The domain cost of any nonzero real scale against itself vanishes. Cosmology and cost-structure arguments cite this to normalize self-comparisons on the recognition ladder. The proof unfolds the cost as J of a ratio, cancels the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of $r$ relative to itself is zero: if domain cost is $J(r/r)$ with $J$ the recognition cost, then $J(1) = 0$.
background
Recognition cost $J$ (also written Jcost) is the unique nonnegative cost fixed by the Recognition Composition Law; one algebraic form is $J(x) = (x-1)^2/(2x)$, so $J(1) = 0$. In this module the domain cost of two positive scales is that cost evaluated on their ratio.
The module is Cosmology RS Structural Module 6: structural theorems (zero sorry, zero axiom) around RS phi uniqueness, the self-similar fixed point $\varphi = 1 + 1/(1+1/(1+\cdots))$. Domain cost supplies the local comparison functional used when checking fixed-point and threshold statements on scales.
Upstream, Jcost_unit0 records exactly $J(1) = 0$, which is the algebraic root needed once a ratio collapses to the unit.
proof idea
One-line wrapper. Unfold domain cost to $J$ of the ratio; rewrite $r/r = 1$ via the nonzero hypothesis; finish by the lemma $J(1) = 0$.
why it matters
Places the trivial self-comparison identity in the cosmology structural layer so later nonnegativity and threshold lemmas can treat equal scales as zero-cost without re-proving the unit root of $J$. No downstream users are wired yet in the graph; the natural parents are sibling facts such as domain-cost nonnegativity and the canonical threshold certificate in the same module.
Framework link: T5 forces uniqueness of $J$, and $J(1) = 0$ is the normalization that makes the self-similar fixed-point story (T6, phi) cost-consistent. The module status line marks the whole file as a closed structural theorem block for phi uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.