domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals (m, e) the recognition cost of their ratio m/e. Anyone deriving RS channel or bandwidth bounds from the forced cost functional would cite it as the local cost of a mass-energy (or signal-noise) ratio. It is a one-line definition: apply J to m/e.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The ambient module develops an RS reading of Shannon capacity $C=B\log_2(1+\mathrm{SNR})$. At $\phi$-resonance the structural SNR is taken to be $\phi^D=\phi^3$, so $C_{\mathrm{RS}}=B\log_2(\phi^3+1)$. Status is structural (no sorry, no axiom).
The cost functional used throughout is $J(x)=\frac{1}{2}(x+x^{-1})-1$, the unique nonnegative cost forced by the Recognition Composition Law (T5). Upstream copies of $J$ state the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Domain cost simply specializes $J$ to a two-argument ratio $m/e$, the natural place to feed mass-to-energy, message-to-noise, or other dimensionless RS ratios into the bandwidth story.
proof idea
Pure definition, no proof obligations. The body is the term $J(m/e)$ with $J$ the standard recognition cost $(x+x^{-1})/2-1$. Sibling lemmas (nonnegativity, evaluation identities) are proved separately from this def.
why it matters
Gives the module a named cost of a two-slot ratio so later bandwidth certificates can speak about thresholds without reopening the definition of $J$. It sits under the structural RS Shannon claim $C_{\mathrm{RS}}=B\log_2(\phi^3+1)$ and inherits the T5 uniqueness of $J$ from the forcing chain. Downstream use is not yet wired in this graph snapshot; siblings such as nonnegativity of domain cost, the canonical threshold, and the BandwidthPhi certificate are the immediate consumers. Landmark tie-in: $J$ is the T5 fixed cost, and $\phi^3$ is the $D=3$ spatial factor from T8 entering the SNR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.