domainCost_at_equilibrium
plain-language theorem explainer
Equal nonzero rates carry zero domain cost: the J-cost of the ratio r/r vanishes. Information theorists working the LDPC capacity-gap argument cite this as the equilibrium baseline against which rate mismatch is measured. The proof is a one-line unfold plus the unit root of J.
Claim. For every real $r \neq 0$, the domain cost of the matched pair $(r,r)$ is zero. Equivalently, writing the domain cost as the J-cost of the ratio of the two arguments, $J(r/r) = J(1) = 0$.
background
The ambient module derives an LDPC designed-rate threshold from the Recognition J-cost. Empirically, well-designed LDPC codes sit 5–15% below Shannon capacity; the module identifies that gap with $J(\varphi) \approx 0.118$.
The J-cost is the unique nonnegative cost forced by the Recognition Composition Law, normalized so $J(1)=0$ and $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$). Domain cost is the local mismatch functional obtained by feeding the ratio of two positive rates into $J$.
Upstream, Jcost_unit0 records the normalization $J(1)=0$, which is the algebraic content of the unit fixed point of the cost.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio of its two arguments). Rewrite the ratio $r/r$ by div_self using the hypothesis $r \neq 0$, obtaining the argument $1$. Discharge with the upstream lemma $J(1)=0$.
why it matters
Supplies the equilibrium baseline for the LDPC-from-J-cost development: any nonzero matched rate pair is cost-free, so all capacity penalty is pure mismatch. That is the natural zero of the gap the module equates with $J(\varphi)\approx 0.118$ (the finite-blocklength LDPC penalty).
In the forcing chain this rests on T5 (J-uniqueness) and the unit normalization of $J$. No downstream consumers are wired yet in the graph; the lemma is scaffolding for the later threshold and certificate objects in the same module (canonicalThreshold, LDPCCert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.