domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Anyone bounding recognition costs or thresholds in the structural count-law module would cite this. The proof is a one-line wrapper: unfold the domain cost to J-cost of the mass-to-energy ratio, then apply J-cost nonnegativity.
Claim. For all real $m,e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)=J(m/e)$ and $J(x)=(x+x^{-1})/2-1$ is the recognition cost.
background
The ambient module is Mathematics RS Structural Module 3, which records the RS count law $2^D-1=7$ independent channels forced by the $D=3$ configuration dimension (forcing chain T8). Status is structural: zero sorry, zero axiom.
The recognition cost $J$ (also written Jcost) is the unique nonnegative cost fixed by the Recognition Composition Law and T5: $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $(x-1)^2/(2x)$. Upstream, Jcost_nonneg states that $J(x)\ge 0$ for every positive $x$, proved by rewriting to a square over a positive denominator (AM-GM).
Domain cost is the local specialization of that cost to a mass-energy ratio: on positive $m,e$ one sets $C_{\mathrm{dom}}(m,e)=J(m/e)$. Nonnegativity of domain cost is therefore the same inequality pulled back along the positive map $(m,e)\mapsto m/e$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. Positivity of the ratio follows from div_pos on the two hypotheses $m>0$ and $e>0$. Discharge the goal by the upstream lemma Jcost_nonneg applied to that positive ratio. No further algebraic work.
why it matters
Keeps every subsequent inequality that mentions domain cost inside the nonnegative cone required by Recognition Science. The module packages the count-law identity $2^D-1=7$ as a structural theorem; nonnegativity of the cost that grades those channels is the elementary positivity fact underneath threshold and certificate constructions in the same file (canonical threshold positivity, the structural certificate).
No downstream theorems currently depend on this declaration in the graph, so it is a leaf positivity lemma rather than a bridge into physics. It still anchors the cost side of the structural layer that sits above T5 (J-uniqueness) and T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.