domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass-energy pair is nonnegative. Cosmology proofs that treat matter-radiation balance as a J-cost on the ratio m/e cite this bound to keep thresholds and certificates well-defined. The argument is a one-line unfold of the domain cost into the standard J-cost, then AM-GM nonnegativity on the positive quotient.
Claim. For all real $m,e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Equivalently, if the domain cost is the J-cost of the ratio $m/e$, then $J(m/e)\ge 0$.
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$ whenever $x>0$, with equality only at $x=1$. That fact is recorded as Jcost_nonneg in the Cost library (and mirrored in gravity bridges): "J(x) ≥ 0 for positive x (AM-GM inequality)".
This module is Cosmology RS Module 7, a structural theorem package for matter-radiation equality at $z_{\mathrm{eq}}\sim\phi^{17}\cdot 0.95\approx 3400$. The local domain cost is the J-cost evaluated on a positive mass-to-energy ratio, so nonnegativity is the first sanity constraint before thresholds and certificates are built.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg to that positive quotient. No further algebraic work.
why it matters
Nonnegativity keeps every downstream comparison of domain cost against a positive canonical threshold meaningful: a cost that could go negative would break the structural certificate for matter-radiation equality in this module. The parent package is the Module-7 cosmology certificate (siblings include the canonical threshold positivity and the inhabited cert). In the broader forcing chain the same J appears at T5 (J-uniqueness) and under the Recognition Composition Law; here it is only the elementary positivity half, specialized to the cosmological mass-energy ratio. No open sorry is discharged; the lemma simply anchors the cost side of the MATCH claim $z_{\mathrm{eq}}\sim 3400$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.