domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Cosmology workers in the Recognition Science structural chain use this when lower-bounding vacuum or domain contributions built from the J-cost. The argument is a one-line unfold of domain cost into J of the mass-to-energy ratio, then the standard AM-GM nonnegativity of J.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ on positive reals (equivalently $(x-1)^2/(2x)$). By AM-GM, $J(x)\ge 0$ whenever $x>0$; that fact is recorded as Jcost_nonneg in the Cost module and re-proved in several gravity bridges.
This file is Cosmology Structural Module 9. Its module doc places it on the forcing chain T5 (J-uniqueness) through T8 ($D=3$), and marks the module as a structural theorem block with zero sorry and zero axioms. The local domain cost is the J-cost of a positive mass-to-energy ratio: unfolding shows $C_{\mathrm{dom}}(m,e)=J(m/e)$.
Upstream, the Cost lemma states exactly "$J(x)\ge 0$ for positive $x$ (AM-GM inequality)" and proves it by rewriting $J$ as a square over a positive denominator.
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 applying the upstream lemma Jcost_nonneg to that positive ratio. No further algebraic work.
why it matters
Nonnegativity of domain cost is the first structural sanity check in RS_COS_Structural_009: every later threshold or certificate in the module (canonical threshold positivity, the inhabited structural certificate) sits on a cost that cannot go negative. The module doc ties the file to the forcing chain T5 J-uniqueness through T8 three-dimensional space, so this lemma keeps the cosmological cost layer consistent with the unique J forced at T5 and the Recognition Composition Law.
No downstream theorems currently list this declaration as a direct dependency, but the sibling certificate bundle (RSCOSStructural009Cert, cert_inhabited) is the natural consumer: a structural cert that quotes domain costs needs the sign bound before it can assert thresholds or vacuum floors. The result closes no open scaffold; it is already a zero-sorry proved fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.