domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is non-negative. Information theorists deriving Shannon capacity from the RS J-cost cite this as the basic positivity lemma. The proof is a one-line wrapper: unfold the domain cost to J of the mass-to-energy ratio, then apply J-cost non-negativity.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
The ambient module builds Shannon channel capacity from the Recognition Science J-cost. The structural claim is $C=B\log_2(1+\mathrm{SNR})$ evaluated at the RS-native SNR $J(\varphi)^{-2}\approx 71.7$, giving roughly $B\cdot 6.18$ bits/s/Hz, close to $\varphi^{2\varphi}$.
The cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique nonnegative generator forced by the Recognition Composition Law and the T5 uniqueness step. Domain cost is the specialization of $J$ to the positive ratio of two real parameters (mass and energy scale in the local naming).
Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
proof idea
One-line wrapper. Unfold domain cost so the goal is non-negativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the standard lemma that $J$ is nonnegative on the positive reals.
why it matters
Positivity of domain cost is the first structural fact needed before thresholds, certificates, and the channel-capacity identity in this module can be stated cleanly. The module is marked structural (zero sorry, zero axioms) and sits in the Information domain of the RS mirror: it converts the forced J-cost into a Shannon-style capacity number at the golden-ratio fixed point.
No downstream consumers are wired yet in the graph, so the lemma is presently a local hygiene fact for the capacity certificate (ChannelCap2Cert and related siblings). It inherits its force from T5 J-uniqueness and the AM-GM form of $J$, rather than from any new physical hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.