domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Researchers packaging RS gap-45 structural facts or any positivity argument for recognition costs would cite it. The proof is a one-line unfold of domain cost to J-cost of the mass/energy ratio, then the standard J-nonnegativity lemma.
Claim. If $m>0$ and $e>0$ are real, then the domain cost of the pair satisfies $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the positive ratio $m/e$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). By AM-GM, $J(x)\ge 0$ with equality only at $x=1$. That fact is recorded as Jcost_nonneg in the Cost module: "$J(x)\ge 0$ for positive $x$ (AM-GM inequality)".
This module is Mathematics RS Structural Module 4. Its local setting is the gap-45 identity $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference at spatial dimension $D=3$. Domain cost is the J-cost evaluated on a positive mass-to-energy ratio $m/e$; the present lemma is the elementary positivity fact for that quantity.
Upstream copies of J-nonnegativity also appear in the gravity coherence and energy-processing bridges; all reduce to the same AM-GM (or squared-form) argument.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is J-cost of the ratio $m/e$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply Jcost_nonneg to that positive quotient. No further algebraic work.
why it matters
Supplies the basic nonnegativity fact inside the gap-45 structural package (minimum rung for stable self-reference at $D=3$). The module is marked STRUCTURAL THEOREM with zero sorry and zero axiom; this lemma is part of that clean positivity layer.
It sits under the T5 J-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) and the T8 forcing of $D=3$. No downstream consumers are wired in the current graph (used_by empty), so it is infrastructure rather than a parent of a named paper proposition. Anyone later bounding domain costs, thresholds, or the canonical threshold siblings in this file will need it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.