domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Structural and gravity modules that treat cost of a mass-to-energy ratio cite this bound. The proof is a one-line wrapper: unfold the domain cost and apply nonnegativity of the J-cost at 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)$. Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$, with $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module records RS structural predictions: the unique cost $J(x)=\frac12(x+1/x)-1$, the golden ratio fixed point, and forced spatial dimension $D=3$, with zero sorry and zero axioms.
The J-cost (also written $J$ or Jcost) is the canonical nonnegative defect on positive reals. Upstream lemmas state $J(x)\ge 0$ for $x>0$, proved by rewriting $J(x)=(x-1)^2/(2x)$ or by AM-GM ($x+x^{-1}\ge 2$). Domain cost is the specialization of that cost to a mass-energy ratio: after unfolding, $C_{\mathrm{dom}}(m,e)=J(m/e)$.
Positivity of the ratio is the only arithmetic prerequisite; once $m/e>0$, the general J-nonnegativity lemma applies verbatim.
proof idea
One-line wrapper. Unfold domainCost so the goal is nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the upstream lemma Jcost_nonneg (AM-GM / square form of $J$).
why it matters
Nonnegativity of domain cost is the first structural sanity check in RS_MTH_Structural_001: cost cannot go negative on physical mass-energy pairs. It sits under the T5 J-uniqueness landmark ($J(x)=\cosh(\log x)-1$) and the Recognition Composition Law, which treat $J$ as the unique admissible defect. No downstream theorems currently depend on this declaration in the graph, so it functions as a local certificate and a reusable bound for later threshold and coherence arguments in the same module (canonical threshold positivity, structural cert inhabitation).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.