domainCost_nonneg
plain-language theorem explainer
For positive mass and energy the cosmological domain cost is nonnegative. Cosmology and gravity arguments that need a free-energy lower bound cite this. The proof is a one-line unfold of the domain cost into the standard J-cost, then AM-GM nonnegativity on the mass-to-energy ratio.
Claim. For all real $m,e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)$ is the recognition $J$-cost of the ratio $m/e$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) on positive reals. By AM-GM, $J(x)\ge 0$ with equality only at $x=1$; this is the lemma Jcost_nonneg in the Cost module (and parallel copies in gravity bridges).
This file is Cosmology RS Structural Module 2. Its local setting is the golden-ratio recognition cost: the unique minimum of $J$ on the self-similar scale sits at $\varphi$, with $J(\varphi)=\varphi-3/2\approx 0.118$. Domain cost is the specialization of $J$ to a positive mass-energy ratio $m/e$, the natural dimensionless argument for cosmological bookkeeping.
Upstream, nonnegativity of $J$ is already proved three ways (square form, field simplification to $(x-1)^2/(2x)$, and the $x+x^{-1}\ge 2$ rearrangement). The present statement simply transports that fact to the cosmology naming.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is exactly $J(m/e)$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the Cost-module lemma that $J(x)\ge 0$ for every positive $x$. No further algebraic work.
why it matters
Nonnegativity of domain cost is the free-energy lower bound needed before any cosmological comparison of recognition costs can be stated. The module frames this as a structural theorem (zero sorry, zero axiom) supporting the golden-ratio minimum $J(\varphi)=\varphi-3/2$.
In the broader forcing chain, $J$-uniqueness is T5 and $\varphi$ is forced at T6; the present lemma is the elementary positivity half of that story, specialized to mass-energy ratios. Sibling certificates (RSCOSStructural002Cert, canonicalThreshold_pos) sit on the same nonnegativity substrate. No downstream consumers are wired yet in the graph, so the lemma currently anchors the module's own certificate rather than a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.