domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost is nonnegative. Cite this when bounding Recognition costs on mass-to-energy ratios in the structural rung-spacing module. The proof is a one-line unfold of domain cost into J-cost of the ratio, then the standard AM-GM nonnegativity of J.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. Equivalently, if $C_{\mathrm{dom}}(m,e)$ is the $J$-cost of the ratio $m/e$, then $J(m/e)\ge 0$.
background
The ambient module is Mathematics RS Structural Module 8: structural theorems (zero sorry, zero axiom) on Recognition Science rung spacing, where adjacent rungs differ by the golden ratio $\varphi\approx 1.618$.
The cost functional $J$ is the unique nonnegative defect from the Recognition Composition Law. Explicitly $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $(x-1)^2/(2x)$. Upstream, Jcost_nonneg records $J(x)\ge 0$ for every positive real $x$, proved by rewriting as a square over a positive denominator (AM-GM).
Here domain cost is the specialization of that $J$-cost to a positive mass-energy pair: after unfolding, $C_{\mathrm{dom}}(m,e)=J(m/e)$. The hypotheses $m>0$ and $e>0$ guarantee the ratio is positive, so the general nonnegativity lemma applies.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the mass-to-energy ratio). Discharge the positivity side-condition on $m/e$ by div_pos from the two strict inequalities, then apply the upstream lemma that $J(x)\ge 0$ whenever $x>0$.
why it matters
Nonnegativity of domain cost is the first structural sanity check in Module 8: costs on rung ratios cannot go negative, matching the global $J\ge 0$ forced at T5 in the Unified Forcing Chain. The module packages this with the canonical threshold and a certificate object (RSMTHStructural008Cert), so later structural claims can assume a well-behaved nonnegative cost on mass-energy pairs without re-proving AM-GM.
No downstream consumers are wired yet in the graph; the lemma exists to close the nonnegativity obligation inside the Module 8 certificate and to keep the phi-ladder cost calculus consistent with the Recognition Composition Law. It does not itself force $\varphi$ or the eight-tick period; those sit upstream in T6-T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.