domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass-energy pair is nonnegative. Workers using recognition costs on mass-to-energy ratios cite this for the zero lower bound. The proof is a one-line unfold of the domain-cost definition, then the standard nonnegativity lemma for the J-cost on the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le J(m/e)$, where $J$ is the recognition cost $J(x)=(x+x^{-1})/2-1$.
background
Foundation Module 9 records structural facts about the recognition cost $J$, notably its ratio symmetry $J(x)=J(1/x)$. Status is a structural theorem block with no sorry and no axioms. In RS, $J$ is the unique cost forced by the Recognition Composition Law; on positives it is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ (T5 J-uniqueness).
Domain cost is the packaging of $J$ on a mass-energy ratio $m/e$. Nonnegativity of $J$ itself is AM-GM: $x+1/x\ge 2$ for $x>0$, so $J(x)\ge 0$ with equality only at $x=1$. Upstream lemmas in Cost (and parallel Gravity copies) state exactly that $J(x)\ge 0$ whenever $x>0$.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$), then apply the library lemma that $J$ is nonnegative on every positive real, feeding the positivity of the quotient $m/e$ from $m>0$ and $e>0$.
why it matters
Nonnegativity is the most basic structural property any RS cost functional must carry. It lives in Foundation Module 9 next to ratio symmetry, inside the forcing-chain material that isolates $J$ (T5) and underwrites later octave and dimension steps. Sibling declarations in the same module (canonical threshold positivity, the module certificate) need a nonnegative domain cost so thresholds and collapse criteria stay well-posed. No downstream used-by edges are recorded yet; the lemma is presently local scaffolding for the module certificate rather than a widely imported API fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.