domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost is nonnegative. Anyone using the RS cost on mass-energy ratios cites this positivity fact. The proof is a one-line wrapper: unfold the domain cost and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \leq J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition J-cost.
background
The Recognition J-cost is $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced unique at T5 of the forcing chain. Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
In this module the domain cost of a mass-energy pair is the J-cost of their ratio: $\mathrm{domainCost}(m,e)=J(m/e)$. The local setting is Mathematics RS Structural Module 9, which sits on the forcing spine T5 (J-uniqueness) through T8 ($D=3$), and is marked structural with zero sorry and zero axioms.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity into the upstream lemma Jcost_nonneg, which closes the goal by the AM-GM form of $J$.
why it matters
Positivity of domain cost is the elementary sign check needed before any comparison of mass-energy configurations against a threshold (siblings include a canonical threshold and its positivity). It sits inside Structural Module 9 on the RS forcing chain T5-T8, so it inherits the J-uniqueness story rather than re-proving it.
No downstream consumers are recorded yet; the lemma is infrastructure for later structural certificates in the same module (the module-level cert and inhabited proof). It does not itself force phi, the eight-tick octave, or $D=3$, but it keeps the cost side of those arguments well-typed and nonnegative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.