domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Cost and coherence arguments in Recognition Science cite this whenever a domain functional must sit above zero. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of the J-cost on the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)=J(m/e)$ and $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
Recognition Science measures mismatch by the J-cost $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. Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
The domain cost packages that same functional on a mass–energy ratio: after unfolding, $C_{\mathrm{dom}}(m,e)$ is exactly $J(m/e)$. The ambient module is the structural mathematics package on $\varphi$-uniqueness (the self-similar fixed point $\varphi=1+1/(1+1/\cdots)$), status structural theorem with zero sorry and zero axiom.
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. Discharge the goal by the upstream lemma Jcost_nonneg on that positive quotient.
why it matters
Positivity of domain cost is the elementary lower bound any later coherence, collapse, or energy-processing argument needs before comparing costs to thresholds. It sits inside the structural mathematics module whose headline is $\varphi$-uniqueness (T6 of the forcing chain), and it reuses the same J-nonnegativity that appears in the gravity coherence-collapse and energy-processing bridges. No downstream consumers are wired yet in the graph; the lemma is infrastructure for any certificate that treats domain cost as a genuine cost rather than a signed residual. It does not itself force $\varphi$ or the eight-tick octave; it only keeps the cost side of those arguments well-founded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.