domainCost_nonneg
plain-language theorem explainer
For strictly positive mass and energy, the domain cost is nonnegative. Structural-cost arguments that treat mass-to-energy ratios as J-cost inputs cite this bound. The proof is a one-line wrapper: unfold the domain cost and apply nonnegativity of J on the positive quotient.
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)=J(m/e)$ with $J(x)=(x+x^{-1})/2-1$, 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. By AM-GM, $J(x)\ge 0$ with equality only at $x=1$; that fact is the upstream lemma Jcost_nonneg.
This module (Mathematics RS Structural Module 2) packages structural facts about that cost, including its value at the golden ratio: $J(\varphi)=\varphi-3/2\approx 0.118$. The domain cost is the specialization of $J$ to a mass-energy ratio $m/e$, so positivity of the ratio is the only hypothesis needed to inherit nonnegativity from $J$.
The local setting is a zero-sorry structural certificate layer: definitions and elementary inequalities that later feed the module certificate, not a dynamical or physical derivation.
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. Finish by applying the upstream lemma that $J(x)\ge 0$ for every positive $x$ (AM-GM / squared form of $J$).
why it matters
Nonnegativity is the first structural filter on any RS cost: without it, a mass-energy domain cost could undercut the forced minimum at $\varphi$ and break the T5 J-uniqueness story ($J(x)=(x+x^{-1})/2-1$). The module frames this as part of the golden-ratio recognition-cost package ($J(\varphi)=\varphi-3/2$).
No downstream theorems currently depend on this declaration in the graph; it sits as a leaf supporting the module certificate (RSMTHStructural002Cert / cert_inhabited) rather than a long forcing-chain step. It closes the elementary positivity obligation so later structural claims can assume a well-behaved nonnegative cost on positive ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.