domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the cosmology domain cost is nonnegative. Anyone treating that cost as a genuine penalty (thresholds, structural certificates) cites this bound. The proof is a one-line unfold to J-cost nonnegativity on the ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition cost (equivalently $\cosh(\log x)-1$).
background
Recognition Science forces a unique nonnegative cost on positive reals: $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. Nonnegativity is the AM-GM content of the upstream lemma Jcost_nonneg: "$J(x)\ge 0$ for positive $x$ (AM-GM inequality)", often proved via the square form $(x-1)^2/(2x)$.
This file is Cosmology RS Structural Module 6, whose theme is the self-similar fixed point $\varphi=1+1/(1+\cdots)$ as a structural theorem pack (0 sorry, 0 axiom). Locally, domainCost of a mass-energy pair is defined as that $J$ evaluated at the ratio $m/e$. Positivity of the ratio is immediate from $m,e>0$, so the cost inherits nonnegativity from $J$.
proof idea
One-line wrapper. Unfold domainCost to expose $J(m/e)$. The hypothesis pair $0<m$ and $0<e$ gives $0<m/e$ by div_pos, and Jcost_nonneg finishes.
why it matters
Structural positivity certificate for the cosmology domain cost inside the RS structural pack on $\varphi$-uniqueness. It underwrites any later comparison of domainCost against a positive threshold (siblings such as canonicalThreshold and the module certificate RSCOSStructural006Cert). Framework landmark: T5 J-uniqueness and the global fact that recognition cost never goes negative on $(0,\infty)$. No used_by edges are recorded yet; the lemma is infrastructure inside the structural module rather than a bridge into a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.