domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Physicists bounding RS Module 5 costs (QCD one-loop structure forced by D=3) cite this as the basic positivity fact. The proof is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$.
background
Recognition Science Module 5 treats the QCD one-loop coefficient $b_0=7=2^D-1$ as forced by the count law once spatial dimension $D=3$ is fixed (forcing chain T8). Costs in this module are built from the standard J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, which is nonnegative for $x>0$ by AM-GM.
The domain cost of a positive mass-energy pair is the J-cost of their ratio. Upstream, Jcost_nonneg records exactly that $J(x)\ge 0$ whenever $x>0$, proved either by rewriting $J$ as a square over a positive denominator or by the elementary inequality $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold the domain-cost definition (so the goal becomes nonnegativity of $J(m/e)$), then apply the upstream lemma that $J$ is nonnegative on positives, feeding it the fact that $m/e>0$ from the two positivity hypotheses via div_pos.
why it matters
Gives the elementary positivity half of the Module 5 cost calculus used when the QCD beta-function coefficient is identified with the count-law value $2^D-1=7$. No downstream theorems currently depend on it in the graph, so it sits as a local structural lemma supporting the module certificate (RSPhysics005Cert) rather than a forcing-chain step. It inherits the T5 uniqueness of $J$ and the T8 dimension count only indirectly, through the ambient Module 5 narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.