domainCost_nonneg
plain-language theorem explainer
The domain cost attached to a positive mass-to-energy ratio is nonnegative. Information and compression arguments in the RS stack cite this to keep overhead terms on the correct side of inequalities. The proof is a one-line wrapper: unfold the domain cost to J of the ratio, then apply AM-GM nonnegativity of J.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the ratio $m/e$ is nonnegative: $0 \leq J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module develops a structural theorem on data-compression rates from the RS J-cost: an RS-optimal code carries entropy $H$ plus a $J(\varphi)$ overhead per symbol (at $H=1$, average length $1.118$ bits/symbol). Domain cost is the local cost functional on a positive mass-energy pair, defined by evaluating $J$ on their ratio.
The J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) is the unique nonnegative cost forced by the Recognition Composition Law and the T5 uniqueness step. Upstream, Jcost_nonneg records the elementary fact 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 the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge the goal by the upstream lemma that $J$ is nonnegative on the positive reals.
why it matters
Keeps every domain-cost term nonnegative inside the Compression3DeepFromJCost package (structural, zero sorry). That package ties RS-optimal code length to entropy plus a forced $J(\varphi)$ overhead, so nonnegativity is the first inequality any rate or certificate argument needs. It sits on the T5 J-uniqueness landmark: once $J$ is the unique cost, its AM-GM nonnegativity is inherited by every derived cost, including domain cost on mass-energy ratios. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the module's compression certificate and threshold lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.