domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass-energy pair is nonnegative. Anyone working with the RS logo cost on the positive ray cites this to keep thresholds and certificates well-defined. The proof is a one-line unfold of the domain cost into the standard J-cost, then AM-GM nonnegativity on the positive ratio.
Claim. For all real $m,e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Equivalently, if $C_{\mathrm{dom}}(m,e)=J(m/e)$ with $J(x)=(x+x^{-1})/2-1$, then $J(m/e)\ge 0$.
background
Recognition Science Logo5 treats the single curve $J(x)=(x+1/x)/2-1$ on $(0,\infty)$ as the structural cost of recognition. It vanishes only at $x=1$ and is the unique cost forced by the Recognition Composition Law (T5 J-uniqueness). The module is a structural theorem file: zero sorry, zero axioms.
The domain cost is the specialization of that $J$ to a positive mass-energy ratio: unfolding shows $C_{\mathrm{dom}}(m,e)=J(m/e)$. Upstream, Jcost_nonneg records the elementary fact that $J(x)\ge 0$ for every $x>0$, proved either by rewriting $J$ as a square $(x-1)^2/(2x)$ or by AM-GM ($x+x^{-1}\ge 2$).
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos, so the standard lemma $J\ge 0$ on positives applies directly and finishes the goal.
why it matters
Nonnegativity is the first structural property of the RS logo curve: the cost never goes below the vacuum value $J(1)=0$. In this module it underwrites the canonical threshold and the Logo5 certificate (canonicalThreshold_pos, RSLogo5Cert, cert_inhabited), ensuring every plotted or certified cost sits on the physical side of the minimum. Framework-wise it is the local positivity half of T5 J-uniqueness and of the RCL identity; without it the phi-ladder yardsticks and the eight-tick octave would not be ordered relative to the vacuum. No downstream edges are recorded yet; the lemma is infrastructure for the Logo5 certificate block itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.