domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Cosmology workers in the RS structural layer use this when bounding recognition costs on the eight-tick lattice. The argument is a one-line unfold of the domain-cost definition, then the standard J-cost nonnegativity lemma on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost $C_{\mathrm{dom}}(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
The module is Cosmology RS Structural Module 5: structural theorems (zero sorry, zero axiom) around the RS eight-tick, the period $2^D=8$ complete traversal of the binary recognition lattice.
The J-cost is the unique nonnegative cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $\cosh(\log x)-1$. Upstream, Jcost_nonneg records $J(x)\ge 0$ for $x>0$, proved via the squared form $(x-1)^2/(2x)$ or by AM-GM ($x+x^{-1}\ge 2$).
Domain cost is the specialization of that cost to a positive mass-energy pair: it is $J(m/e)$. Nonnegativity of the ratio $m/e$ is immediate from positivity of both arguments.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is J-cost of the ratio $m/e$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma that J-cost is nonnegative on every positive real (AM-GM / squared form). Done.
why it matters
Keeps the cosmology structural certificate free of sign leaks: every domain-cost appearance in the eight-tick layer is known nonnegative before any threshold or comparison is written. The module status line marks this as a structural theorem in the RS-COS series tied to the eight-tick octave (forcing-chain T7: period $2^3=8$).
No downstream consumers are wired in the graph yet; sibling names show it sits beside the domain-cost definition, the equality-at-evaluation lemma, the canonical threshold and its positivity, and the module certificate RSCOSStructural005Cert. It is the elementary positivity brick those objects rely on when they treat domain cost as a genuine cost rather than a signed defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.