domainCost
plain-language theorem explainer
Domain cost measures the recognition penalty of a measured quantity against an expected baseline by feeding their ratio into the unique J-cost. Information theorists working the LDPC rate-gap argument cite it as the scalar that turns a rate mismatch into a nonnegative cost. The body is a one-line abbreviation of J on the ratio.
Claim. For real numbers $\mathrm{measured}$ and $\mathrm{expected}$, the domain cost is $J(\mathrm{measured}/\mathrm{expected})$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The module derives an LDPC code-rate threshold from Recognition Science cost. Status is structural: zero sorry, zero axiom. The empirical claim is that well-designed LDPC codes sit within about 5–15% of Shannon capacity, and the RS gap scale is $J(\varphi)\approx 0.118$.
The cost functional is the forced J-cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream docs state it is the unique cost forced by the Recognition Composition Law, nonnegative for positive $x$, and strictly positive off the equilibrium ratio $x=1$. Domain cost simply specializes that functional to a measured-versus-expected ratio in the coding setting.
proof idea
Pure definitional abbreviation: apply $J$ to the single ratio $\mathrm{measured}/\mathrm{expected}$. No lemmas, no tactics, no side conditions are discharged at this declaration; nonnegativity and equilibrium vanishing appear in sibling lemmas.
why it matters
This is the scalar interface between coding-theory rate mismatch and the RS cost calculus. Sibling results (equilibrium vanishing, nonnegativity, the canonical threshold, and the LDPC certificate) all read domain cost as their primitive. In the forcing chain it inherits T5 J-uniqueness and the RCL shape of $J$, so the LDPC capacity penalty is not an ad-hoc fit but the same functional that forces $\varphi$, the eight-tick octave, and $D=3$. Downstream certificate constructions in the module use it to pin the $\approx 11.8%$ finite-blocklength gap to $J(\varphi)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.