domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the cosmology domain cost is nonnegative. Anyone building or citing the RS Cosmology Module 1 certificate stack (Omega_Lambda structural match) uses this bound as a basic sanity check. The proof is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio.
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 $J$ is the Recognition Science cost $J(x)=(x+x^{-1})/2-1$.
background
Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. Equivalently $J(x)=(x-1)^2/(2x)$; nonnegativity is the AM-GM inequality (upstream lemma: "$J(x)\ge 0$ for positive $x$").
This file is Cosmology RS Module 1, a structural (zero-sorry) package for the dark-energy density claim $\Omega_\Lambda=11/16-\alpha/\pi\approx 0.685$, matching Planck at $0.665\sigma$. Domain cost is the local cost functional obtained by evaluating $J$ on a positive mass-to-energy ratio $m/e$.
Sibling facts in the module include the definition of domain cost, its evaluation identity, a canonical threshold, and the inhabited certificate RSCosmo001Cert.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio $m/e$), then apply the upstream lemma that $J(x)\ge 0$ whenever $x>0$. Positivity of the ratio is immediate from div_pos on the hypotheses $m>0$ and $e>0$.
why it matters
Nonnegativity of domain cost is a prerequisite sanity bound for any threshold comparison in the cosmology certificate layer (siblings: canonical threshold positivity, RSCosmo001Cert). The module targets the structural $\Omega_\Lambda$ match reported as RS_PASS against Planck.
No recorded downstream dependents yet; the lemma underwrites local cost comparisons rather than a named parent theorem. It inherits the T5 landmark: the same unique $J$ forced by the Recognition Composition Law remains the cost measure when RS is specialized to cosmology. Equality at $m=e$ is the zero-defect fixed point of that cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.