domainCost
plain-language theorem explainer
Domain cost assigns to a message scale m and error scale e the recognition cost of their ratio. Anyone deriving RS error-correction capacity from the Hamming bound uses this as the cost of distinguishing codeword magnitude from noise magnitude. The body is a one-line abbreviation of the forced J-cost on positive reals.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The module treats error-correction capacity as a structural consequence of the RS cost functional. The Hamming bound $2^{n-k}\ge V_H(n,t)$ is read at the RS rate $R=J(\varphi)\approx 0.118$, which supports an error fraction $t/n=J(\varphi)/2\approx 0.059$.
The upstream object is the recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ (also written $\cosh(\log x)-1$). It is the unique cost forced by the Recognition Composition Law (T5 in the forcing chain): nonnegative for $x>0$, zero only at ratio one, and strictly positive for any genuine distinction.
Domain cost simply evaluates that functional on the ratio of a message scale to an error scale, so the same $J$ that prices distinctions in the foundation prices the code-versus-noise distinction in the information layer.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is defined to be $J(m/e)$. No lemmas, no tactics; the body is the single application of the upstream $J$-cost to the ratio.
why it matters
Gives the information module a named cost for the message-to-error ratio, so later certificates (nonnegativity, evaluation at equality, the canonical threshold, and the three-deep error-correction certificate) can speak in domain language rather than raw $J$.
It sits on the T5 uniqueness of $J$ and feeds the structural Hamming reading at rate $J(\varphi)$. The module claims a zero-sorry structural theorem: at that rate the code supports error fraction $J(\varphi)/2$. Domain cost is the local cost object that makes those statements about $(m,e)$ rather than abstract ratios.
No external used-by edges are recorded; the immediate consumers are the sibling lemmas and the inhabited certificate in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.