domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Structural and gravity modules that treat mass-to-energy ratios as J-cost arguments cite this bound. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J on the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0\le J(m/e)$, where domain cost is the J-cost of the mass-to-energy ratio.
background
Module RS_FDN_Structural_009 sits in the Foundation forcing chain (T5 J-uniqueness through T8, D=3). It records structural facts with zero sorry and zero axioms.
The J-cost is $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg states $J(x)\ge 0$ for positive $x$, proved by rewriting as a square over a positive denominator (AM-GM). Domain cost is the specialization of that cost to a mass-to-energy ratio: it unfolds to $J(m/e)$.
The local setting therefore only needs positivity of $m$ and $e$ so that the ratio is a legitimate J-argument.
proof idea
One-line wrapper. Unfold domainCost to expose $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 on that positive ratio.
why it matters
Keeps the structural certificate of module 9 honest: every cost that appears in the mass–energy domain is a genuine nonnegative J-cost, consistent with T5 (J-uniqueness and the AM-GM form). The sibling certificate RSFDNStructural009Cert packages this with the related positivity of the canonical threshold. No downstream consumers are wired yet; the lemma is infrastructure for later gravity and energy-processing bridges that already re-prove or import the same J-nonnegativity fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.