domainCost_nonneg
plain-language theorem explainer
For positive reals m and e, the domain cost built from their ratio is nonnegative. Cosmology auditors and anyone chaining cost bounds in RS Module 2 cite this as the basic positivity fact. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive quotient 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 $J$ is the Recognition J-cost.
background
RS Cosmology Module 2 is a structural (zero-sorry) package around the dimensionless combination $\Lambda \ell_P^2$, claimed to equal $8\varphi^5/45$ and to land in $(1.88,2.03)\times 10^{-122}$, matching Planck's $\sim 1.99\times 10^{-122}$.
The cost functional in play is the standard Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), defined for $x>0$. Upstream, Jcost_nonneg records that $J(x)\ge 0$ on the positive reals, proved by rewriting $J$ as a square over a positive denominator (AM-GM / $(x-1)^2/(2x)$).
Here the domain cost of a mass-like scale $m$ and an energy-like scale $e$ is just that J-cost evaluated at the positive ratio $m/e$. Positivity of the arguments is the only hypothesis needed to place the ratio in the domain of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$), then apply the upstream lemma that $J$ is nonnegative on positive reals, feeding it the fact that $m/e>0$ via div_pos from the two strict positivity hypotheses.
why it matters
This is the elementary positivity lemma for the cost that Module 2 attaches to cosmological domain data. It sits among the structural theorems that underwrite the RS pass on $\Lambda\ell_P^2\in(1.88,2.03)\times 10^{-122}$ and the certificate objects in the same file. No downstream dependents are recorded yet; the lemma is infrastructure so later bounds can quote $0\le$ domain cost without re-proving AM-GM. In the broader forcing chain it inherits T5 J-uniqueness: the same $J$ that is forced as the unique cost appears here as a nonnegative cosmological bookkeeping term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.