domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Cosmology arguments that treat that cost as a J-cost on the mass-to-energy ratio cite this bound before thresholds or certificates. Proof is a one-line unfold plus standard nonnegativity of J on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)=J(m/e)$ and $J(x)=\frac{x+x^{-1}}{2}-1$.
background
Recognition Science measures mismatch with the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ for $x>0$. Upstream, Jcost_nonneg records that $J(x)\ge 0$ on positives, via AM-GM or the squared identity $J(x)=(x-1)^2/(2x)$.
In this cosmology module the domain cost of a mass–energy pair is that same $J$ at the ratio $m/e$. The module targets the scalar spectral index $n_s=1-2/45=0.9556$ versus Planck $0.9649$ (about $2.2\sigma$ tension) and is tagged OPEN as a structural package with zero sorry and zero axioms.
Sibling definitions include the domain-cost function itself, its evaluation identity, a canonical threshold, and the module certificate RSCosmo004Cert.
proof idea
One-line wrapper. Unfold domain cost to expose $J(m/e)$. Positivity of $m$ and $e$ gives $m/e>0$ by div_pos, so the upstream lemma that $J$ is nonnegative on positives finishes the goal.
why it matters
Supplies the elementary nonnegativity fact needed before any threshold or certificate that treats domain cost as a genuine cost in Cosmology Module 4. Siblings canonicalThreshold_pos and RSCosmo004Cert sit in the same structural layer aimed at the open $n_s$ comparison with Planck.
The graph currently lists no downstream users, so this is infrastructure rather than a cited lemma in a larger proof. It rests on the T5 landmark that $J$ is the unique cost functional, whose nonnegativity is the content of the applied upstream result. It does not itself compute $n_s$ or close the tension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.