domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Cosmology proofs that keep the RS baryon-density cost in the physical cone cite this bound. The argument is a one-line unfold of the definition followed by the standard J-cost nonnegativity lemma on the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition J-cost.
background
Recognition Science measures mismatch by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream lemmas record that $J(x)\ge 0$ whenever $x>0$, by AM-GM or by rewriting $J(x)=(x-1)^2/(2x)$.
In this cosmology module the domain cost of a mass-energy pair $(m,e)$ is defined to be exactly that J-cost evaluated at the ratio $m/e$. The module itself is the structural baryon-density identity $J(\varphi)(1-J(\varphi))/2\approx 0.052$, compared with the observed $\Omega_b\approx 0.0493$; nonnegativity of the cost is the elementary positivity guard for every such ratio that appears.
The local setting is therefore pure cost calculus inside RS units, with no dynamical evolution yet.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity witness into the imported lemma Jcost_nonneg, which is the AM-GM form of $J\ge 0$ on the positive reals.
why it matters
Module 9 is marked STRUCTURAL (zero sorry, zero axiom) and supplies the baryon-density match $J(\varphi)(1-J(\varphi))/2\sim\Omega_b$. Nonnegativity of the domain cost is the elementary cone membership fact that keeps every intermediate ratio inside the regime where the T5 J-cost is well-defined and nonnegative. It sits under the same J-uniqueness landmark that forces $J(x)=\cosh(\log x)-1$ and under the Recognition Composition Law. No downstream theorems are recorded yet; the lemma is scaffolding for the module certificate RSCosmo009Cert and any later comparison of predicted versus observed $\Omega_b$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.