domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Lattice and cost-functional arguments in the RS foundation layer cite this to treat domain cost as a genuine cost. 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 $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
Recognition Science takes the scalar cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) as the unique generator of physical predictions. For $x>0$, AM-GM gives $J(x)\ge 0$, with equality only at $x=1$. The same fact is recorded upstream as $J$-cost nonnegativity, proved by rewriting $J(x)=(x-1)^2/(2x)$ or by the elementary bound $x+x^{-1}\ge 2$.
This module (Foundation RS Module 1) packages structural theorems for the recognition lattice with zero sorry and zero axiom. Domain cost is the specialization of $J$ to a positive mass-to-energy ratio $m/e$; the present lemma is the corresponding nonnegativity statement.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$), then apply the upstream lemma that $J(x)\ge 0$ for every $x>0$, feeding it the positivity of the quotient $m/e$ from div_pos on the two hypotheses.
why it matters
Nonnegativity is the first structural property any cost on the recognition lattice must have; without it, domain-level bookkeeping cannot serve as an energy-like functional. The lemma lives in the certified base of Foundation RS Module 1 (status: structural theorem, 0 sorry, 0 axiom), alongside the domain-cost definition, the canonical threshold, and the module certificate. It underwrites the T5 J-uniqueness landmark ($J(x)=\frac{x+x^{-1}}{2}-1$) by confirming that the specialized cost inherits the sign of $J$. No downstream uses are recorded in the graph yet; the result is infrastructure for later forcing-chain and coherence arguments rather than a parent theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.