domainCost_at_eq
plain-language theorem explainer
When both arguments of the domain cost are the same nonzero real, the cost is exactly zero. Anyone deriving Shannon capacity from the RS J-cost cites this as the matched-scale baseline (zero defect). The proof unfolds the cost to J of the ratio, collapses the ratio to 1, and applies the unit root of J.
Claim. For every real $r \neq 0$, the domain cost at equal arguments vanishes: if the cost is the J-cost of the ratio of its two inputs, then that value at $(r,r)$ is $J(1)=0$.
background
This module builds Shannon channel capacity from the Recognition Science J-cost. The structural claim is that at the RS-native SNR fixed by $J(\varphi)^{-2}\approx 71.7$, one obtains $C=B\log_2(72.7)\approx B\cdot 6.18$ bits/s/Hz, a figure near $\varphi^{2\varphi}$.
Domain cost is the J-cost of a ratio of two real scales. The underlying cost is the unique RS functional $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$), forced by the Recognition Composition Law and T5. Its unit root is elementary: $J(1)=0$.
Upstream, Jcost_unit0 records exactly that root: "$J(x)$ expressed as a squared ratio" specializes at $x=1$ to zero by simplification of the definition.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(r/r)$. Rewrite the ratio to $1$ by div_self (using $r\neq 0$). Finish by the upstream unit-root lemma $J(1)=0$.
why it matters
Zero cost on the diagonal is the matched-scale baseline for the information layer: SNR and capacity are measured relative to this vanishing defect. The module status is structural (0 sorry, 0 axiom) and ties capacity to the forced J-cost and the golden ratio via $J(\varphi)$. No used_by edges are recorded yet; sibling results cover nonnegativity, the canonical threshold, and the ChannelCap2Cert certificate that packages the capacity claim. Landmark contact is T5 (J-uniqueness) and the RCL, which fix the cost whose unit root is used here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.