domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Structural and calibration arguments that treat mass-to-energy ratios as J-cost inputs cite this bound. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
In Recognition Science the elementary cost is the J-function $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the forcing chain. For $x>0$, $J(x)\ge 0$ by AM-GM (or by rewriting $J(x)=(x-1)^2/(2x)$).
This module is Mathematics RS Structural Module 10: E_coh is fixed once from the electron mass, after which predictions are parameter-free. The local domain cost is the specialization of J to a positive mass-to-energy ratio, so nonnegativity is inherited from the global J-cost lemma rather than proved from scratch.
proof idea
One-line wrapper. Unfold domainCost to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg (AM-GM form: $J(x)\ge 0$ for $x>0$) to that ratio.
why it matters
Nonnegativity of domain cost is a structural sanity check inside RS_MTH_Structural_010: costs used for mass–energy calibration cannot go negative. It sits under the T5 J-uniqueness landmark and the global Cost development (Jcost_nonneg). Sibling certificates (RSMTHStructural010Cert, cert_inhabited) package this module as a zero-sorry structural theorem. No downstream consumers are recorded yet; the lemma is infrastructure for later calibration and threshold arguments in the same file (canonical threshold positivity, domain-cost evaluations).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.