domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the cosmological domain cost is non-negative. Cosmology workers in the RS module-5 r-tensor consistency check cite this bound when they need a cost that cannot go negative. The proof is a one-line wrapper: unfold the definition and apply J-cost non-negativity to the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$, i.e. $J(m/e)$ with $J(x)=(x+x^{-1})/2-1$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and non-negative on $(0,\infty)$ by AM-GM. The Cost module records this as $J(x)\ge 0$ whenever $x>0$.
This file is Cosmology RS Module 5, a structural (zero-sorry) certificate that the r-tensor value $2/(44\phi^2)\approx 0.0174$ lies below the Planck bound $0.036$. The local domain cost is the J-cost of a positive mass-to-energy ratio: after unfolding, $\mathrm{domainCost}(m,e)=J(m/e)$.
Upstream, three parallel $J\ge 0$ lemmas (Cost, CoherenceCollapse, EnergyProcessingBridge) all state the same fact: for $x>0$, $0\le J(x)$, proved either by rewriting $J$ as a square over a positive denominator or by the elementary inequality $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold domainCost so the goal becomes $0\le J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity into Jcost_nonneg (the Cost-module AM-GM form) and close.
why it matters
Module 5 is a structural consistency certificate for the cosmological r-tensor against the Planck bound. Non-negativity of the domain cost is the elementary positivity lemma that keeps every cost term in that certificate on the correct side of zero; without it the comparison $2/(44\phi^2)<0.036$ would not be a cost bound.
In the broader framework this is an instance of T5 J-uniqueness: the same $J$ that is forced by the Recognition Composition Law remains non-negative when specialized to mass/energy ratios in cosmology. No downstream theorems currently depend on this declaration (used_by is empty); it sits as local scaffolding for the module's own RSCosmo005Cert and related threshold lemmas (canonicalThreshold_pos).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.