domainCost
plain-language theorem explainer
The domain cost of two reals is the recognition cost of their ratio: J(m/e). Workers on the RS Shannon bridge use it to turn a magnitude-to-energy ratio into the unique T5 cost that sets the structural SNR. The body is a one-line specialization of J, not a derived identity.
Claim. For real numbers $m$ and $e$, define the domain cost by $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
The ambient module builds Shannon channel capacity from the RS cost functional. Classical capacity is $C=B\log_2(1+\mathrm{SNR})$; the RS claim is that a structural operating point sits at $\mathrm{SNR}=J(\varphi)^{-2}\approx 71.7$, giving $C=B\log_2(72.7)\approx B\cdot 6.18$ bits/s/Hz, close to $\varphi^{2\varphi}$.
The cost in play is the unique T5 functional $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law. Upstream docs state it as "the RS recognition cost of a positive ratio" and "the unique cost functional forced by the Recognition Composition Law." Domain cost simply feeds the ratio $m/e$ into that $J$.
proof idea
Pure definition: apply the standard $J$-cost to the quotient $m/e$. No lemmas, no tactics, no side conditions at the definition site. Non-negativity and evaluation identities appear only in sibling lemmas.
why it matters
This is the local dictionary entry that turns a two-parameter domain (message scale over energy scale) into a single $J$-number for the channel-capacity certificate in the same module. The module status line marks a structural theorem with zero sorry and zero axioms: at the RS SNR fixed by $J(\varphi)^{-2}$, capacity collapses to $B\log_2(72.7)\approx B\cdot 6.18$, compared with $\varphi^{2\varphi}$. Downstream siblings (domainCost_nonneg, canonicalThreshold, ChannelCap2Cert) rest on this abbreviation so the capacity argument never re-opens the T5 uniqueness proof. It sits on the information side of the forcing chain after T5 $J$-uniqueness and the golden fixed point $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.