domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass-to-energy ratio is non-negative. Compression-ratio work in the RS information layer cites this to keep cost terms on the correct side of inequalities. Proof is a one-line wrapper: unfold the domain-cost definition and apply J-cost non-negativity on the positive quotient m/e.
Claim. For all real $m,e>0$, one has $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ denotes the J-cost of the ratio $m/e$.
background
The module treats the RS compression ratio: maximum lossless compression is the Kolmogorov limit, and RS claims an achievable factor $J(\varphi)^{-1}\approx 8.47$ for structured data at $\varphi$-rung complexity (random data stays at factor 1).
The cost is the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), forced unique at T5 of the unified forcing chain. Upstream, J-cost non-negativity states $J(x)\ge 0$ for every $x>0$, proved by AM-GM or the squared identity $(x-1)^2/(2x)$.
Domain cost is simply that J-cost evaluated on the mass-energy ratio $m/e$, the scale variable used by the compression certificate in this file.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(m/e)$. From $m>0$ and $e>0$, the quotient $m/e$ is positive by div_pos, so the upstream lemma that $J$ is non-negative on positive reals applies directly.
why it matters
Supplies the elementary positivity half of any cost bound inside the module's compression-ratio certificate (siblings CompressionRatioCert, cert). That certificate encodes the RS claim that structured $\varphi$-rung data compresses by $J(\varphi)^{-1}$ while random data remains incompressible. Without non-negativity the Kolmogorov-style comparison is not well-posed. No recorded downstream dependents yet; the lemma is local support for the cert constructors. Landmark link: T5 J-uniqueness (and the RCL that forces $J$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.