domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Cosmology structural proofs that treat domain cost as a J-cost on the mass-to-energy ratio cite this bound before comparing to thresholds. The argument is a one-line unfold plus the standard AM-GM nonnegativity of J on the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$.
background
Module RS_COS_Structural_008 records structural facts for Recognition Science cosmology under the rung-spacing convention that adjacent rungs differ by the golden ratio $\varphi\approx 1.618$. Status is fully proved (no sorry, no axioms).
The J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique nonnegative cost forced by the Recognition Composition Law and T5. Upstream lemmas establish $J(x)\ge 0$ for every $x>0$ by rewriting $J$ as a square over a positive denominator (AM-GM).
In this module the domain cost of a mass-energy pair is the J-cost of their positive ratio. Nonnegativity of that cost is the elementary positivity fact needed before any comparison with canonical thresholds on the $\varphi$-ladder.
proof idea
One-line wrapper. Unfold the definition of domain cost, which is $J$ of the ratio $m/e$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg (AM-GM form from Cost, or the equivalent Gravity restatements) to conclude $0\le J(m/e)$.
why it matters
Structural Module 8 packages the elementary positivity facts that cosmology certificates rely on when domain cost is compared to rung-spacing thresholds. The result sits under the T5 J-uniqueness landmark: once $J$ is forced, every derived cost inherits nonnegativity for free.
No downstream consumers are wired yet in the graph (used_by empty), so the lemma presently closes the local certificate RSCOSStructural008Cert rather than feeding a named parent theorem. It is the positivity half of the domain-cost interface that later threshold comparisons (canonical threshold positivity, certificate inhabitance) presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.