domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the cosmological domain cost is nonnegative. Anyone building or citing the RS Module-6 dark-matter mass scaffold (M_W/45 band, XENONnT falsifier) needs this sign fact. The proof is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio m/e.
Claim. Let $m,e\in\mathbb{R}$ with $m>0$ and $e>0$. Then the domain cost of the pair $(m,e)$ satisfies $0\le J(m/e)$, where $J$ is the Recognition J-cost $J(x)=(x+x^{-1})/2-1$.
background
Module RS_Cosmo_Module_006 is a structural cosmology block aimed at a dark-matter mass prediction near $M_W/45\approx 1.787,\mathrm{GeV}$, flagged as XENONnT-testable. It packages a domain cost on positive mass/energy pairs together with a canonical threshold and a certificate object.
The underlying cost is the Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law. Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM / $(x-1)^2/(2x)$).
In this module the domain cost of $(m,e)$ is exactly $J(m/e)$. Positivity of the ratio follows from the two strict positivity hypotheses, so the Cost-layer nonnegativity lemma applies directly.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J(m/e)$), then apply the Cost lemma that $J(x)\ge 0$ whenever $x>0$, feeding the positivity certificate div_pos hm he for the ratio $m/e$.
why it matters
Nonnegativity is the first structural sanity check on the Module-6 domain cost before thresholds and certificates are built. The module status line marks the whole file as a structural theorem block (zero sorry, zero axiom) supporting the RS dark-matter mass claim $M_W/45$ and its 2026 XENONnT falsifier. No downstream consumers are wired yet in the graph; the lemma sits as local infrastructure so later threshold comparisons and certificate inhabitation proofs can quote a clean $0\le\mathrm{domainCost},m,e$ fact without reopening the AM-GM argument. It inherits the T5 J-uniqueness pedigree only indirectly, through the shared Cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.