domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the cosmological domain cost is nonnegative. Anyone bounding reionization-scale costs in the RS cosmology stack cites this. The proof is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the cosmological domain cost of the pair $(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), defined for $x>0$. Upstream lemmas record that $J(x)\ge 0$ on the positive reals, by AM-GM or by rewriting $J(x)=(x-1)^2/(2x)$.
This module is Cosmology RS Module 8 (reionization). The structural claim is that the $\phi^4$–$\phi^5$ window $6.85$–$11.09$ matches observed reionization redshifts $z_{\mathrm{reion}}\sim 7$–$10$. The local domain cost packages J-cost on a positive mass-to-energy ratio, so nonnegativity is the first algebraic sanity check before threshold comparisons.
proof idea
One-line wrapper. Unfold the definition of the domain cost (which is J-cost of the ratio $m/e$), obtain positivity of $m/e$ from div_pos on the two hypotheses $m>0$ and $e>0$, then apply the upstream lemma Jcost_nonneg.
why it matters
Module 8 is marked STRUCTURAL THEOREM (zero sorry, zero axiom). Nonnegativity of the domain cost is the elementary lower bound needed before comparing that cost to the canonical reionization threshold on the $\phi$-ladder. Sibling certificates (RSCosmo008Cert, cert_inhabited) sit in the same file; this lemma supplies the sign fact those certificates rely on when they assert the $\phi^4$–$\phi^5$ match to $z_{\mathrm{reion}}\sim 7$–$10$. No further downstream edges are recorded yet; the result is local infrastructure for the reionization window, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.