domainCost_nonneg
plain-language theorem explainer
For positive mass and energy the domain cost is nonnegative. Cosmology arguments that treat domain cost as a genuine defect measure cite this fact. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le \mathrm{cost}_{\mathrm{dom}}(m,e)$.
background
Recognition Science measures multiplicative mismatch by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\frac{(x-1)^2}{2x}$). By AM-GM, $J(x)\ge 0$ for every $x>0$, with equality only at $x=1$. That fact is recorded as the upstream lemma on J-cost nonnegativity.
In this module the domain cost of a mass-energy pair is the J-cost of the ratio $m/e$. The surrounding file is Cosmology RS Module 3: it certifies that the local-to-CMB Hubble ratio lies in $(1.075,1.091)$, with the SH0ES value $1.0837$ inside the band (structural theorem, zero sorry, zero axiom).
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). The two positivity hypotheses give $m/e>0$ by division-positivity, and the standard J-cost nonnegativity lemma finishes the goal.
why it matters
Domain cost must be a true cost before any threshold or certificate in the module can treat it as a defect. Sibling declarations such as the canonical threshold positivity and the RSCosmo003 certificate sit on top of that nonnegativity. The lemma is the local nonnegativity hinge for Module 3's Hubble-tension band; no external dependents are recorded yet. It inherits the T5 landmark: the same unique J forced by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.