domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the gravity-side domain cost is nonnegative. Anyone treating that cost as a J-cost on the mass-to-energy ratio cites this bound before coherence or tidal estimates. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$, defined as the J-cost of the ratio $m/e$, is nonnegative: $0 \le J(m/e)$.
background
The Gravity module (RS session 3) is marked structural: zero sorry, zero axioms. Its local benchmark is neutron-star tidal deformability, with the RS ladder value $\phi^{13}\approx 521$ sitting inside the observational window $\Lambda_T\sim 500$–$1000$.
Domain cost is the specialization of the Recognition J-cost to a mass–energy ratio. The J-cost itself is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique nonnegative cost forced by the Recognition Composition Law and recorded as T5 in the forcing chain.
Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as the square $(x-1)^2/(2x)$ or by AM-GM on $x+x^{-1}\ge 2$. That lemma is what the present result instantiates.
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. Feed that positivity into Jcost_nonneg to conclude $0\le J(m/e)$.
why it matters
Supplies the first structural inequality on the gravity domain cost so later coherence-collapse and energy-processing arguments can treat it as a genuine cost rather than a signed defect. The module’s tidal-deformability certificate ($\Lambda_T\sim\phi^{13}$) sits downstream of this cost layer even though no direct used_by edge is recorded yet.
In the broader framework the result is the gravity-side shadow of T5 J-uniqueness: once J is forced, nonnegativity is immediate and must hold on every positive ratio that appears as a domain cost. It does not close an open question; it is local infrastructure that keeps the gravity cost layer honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.