domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost is nonnegative. Cosmology proofs that treat domain cost as a J-cost on the mass-to-energy ratio cite this bound before comparing costs to thresholds. The argument is a one-line wrapper: unfold the definition and apply nonnegativity of J to the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le J(m/e)$, where domain cost is the J-cost of the mass-to-energy ratio.
background
Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Upstream nonnegativity lemmas record $J(x)\ge 0$ for every $x>0$, via the squared identity $J(x)=(x-1)^2/(2x)$ or AM-GM. In this Cosmology module the domain cost of a mass-energy pair is defined by evaluating that same J-cost at the ratio $m/e$.
The module is a structural cosmology layer (zero sorry, zero axioms). Its headline claim is that the dark-energy equation-of-state parameter satisfies $w=-1$ exactly from the RS vacuum; a DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify the framework. Current DESI BAO values ($w_0\approx -0.95$, $w_a\approx -0.27$) show mild tension but not yet a $2\sigma$ break.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). Positivity of $m$ and $e$ gives positivity of the ratio via div_pos. Feed that hypothesis to the upstream lemma that $J(x)\ge 0$ for all $x>0$, and close.
why it matters
Elementary positivity fact inside the RS Cosmology stack that forces $w=-1$ from the vacuum. No recorded downstream dependents yet; it sits with the domain-cost definition, the equality-at-evaluation lemma, the canonical threshold, and the EOSDeep4 certificate siblings. Any later comparison of domain cost against a positive threshold needs this sign bound first. The underlying J is the unique cost forced at T5 of the forcing chain (and obeys the Recognition Composition Law), so the nonnegativity here is the same AM-GM fact that underwrites cost arguments across the monolith, specialized to the cosmological mass-energy ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.