domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Structural and gravity modules that bound recognition cost against thresholds cite this fact. The proof is a one-line wrapper: unfold the domain cost to the J-cost of the mass-to-energy ratio, then apply J-cost nonnegativity (AM-GM).
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)$ is the J-cost of the ratio $m/e$.
background
The module is Foundation RS Structural Module 4, the gap-45 structural theorem: at spatial dimension $D=3$ one has $D^2(D+2)=9\cdot 5=45$, the minimum rung for stable self-reference. Status is a pure structural theorem (no sorry, no axioms).
The J-cost is the standard Recognition cost $J(x)=(x+x^{-1})/2-1$ on positive reals (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg records that $J(x)\ge 0$ for $x>0$, proved by rewriting $J$ as a square over a positive denominator and applying positivity (AM-GM).
Domain cost is the local specialization of that cost to a mass-energy pair: after unfolding, $C_{\mathrm{dom}}(m,e)=J(m/e)$. The positivity hypotheses on $m$ and $e$ guarantee that the ratio is positive, so the upstream lemma applies.
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. Discharge the goal by exact Jcost_nonneg on that positive ratio. No further algebraic work; all content sits in the upstream nonnegativity lemma.
why it matters
Nonnegativity of domain cost is the elementary positivity gate for the gap-45 structural layer: costs that feed threshold comparisons (canonical threshold, stable self-reference at $D=3$) must sit above zero. It sits under the T5 J-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) and the T8 forcing of three spatial dimensions that produces the numerical identity $D^2(D+2)=45$.
No downstream consumers are wired yet in the graph (used_by is empty); the sibling certificate RSFDNStructural004Cert and the positive canonical-threshold lemmas are the natural landing sites. The result closes a trivial but mandatory positivity obligation so later structural inequalities do not re-prove AM-GM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.