domainCost_nonneg
plain-language theorem explainer
The domain cost attached to a positive mass–energy pair is nonnegative. Structural-calibration and energy-processing arguments in the RS foundation cite this as the basic sign check on that cost. The proof is a one-line wrapper: unfold the domain cost to J of the mass-to-energy ratio and invoke nonnegativity of J on positive reals.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. Equivalently, if $C_{\mathrm{dom}}(m,e)$ is the $J$-cost of the ratio $m/e$, then $J(m/e)\ge 0$.
background
Recognition Science measures mismatch by the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) on positive reals. Upstream, $J(x)\ge 0$ for $x>0$ is the AM–GM form of that cost (Cost.Jcost_nonneg and the gravity-side copies).
In this structural module the domain cost of a mass–energy pair $(m,e)$ is that same $J$ evaluated at the ratio $m/e$. The module’s setting is RS calibration: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. Nonnegativity of domain cost is the elementary sign fact needed before any threshold or certificate comparison.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg to that positive ratio and finish.
why it matters
Structural Module 10 packages the RS calibration story (E_coh fixed by the electron, then parameter-free predictions) as a zero-sorry certificate. Nonnegativity of domain cost is the first sign lemma in that package: every later comparison against a canonical threshold or certificate bound needs $C_{\mathrm{dom}}\ge 0$ as a baseline.
It sits on the T5 $J$-uniqueness landmark: once $J$ is forced, its AM–GM nonnegativity is inherited by every derived cost, including the domain cost used in energy-processing and coherence-collapse bridges. No downstream theorems currently list this declaration as a direct dependency, so its role is local infrastructure inside the structural certificate rather than a named step in a longer forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.