domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost built from their ratio is nonnegative. Cost-functional and forcing-chain arguments that need a lower bound on this quantity cite the result. 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.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ (the $J$-cost of the ratio $m/e$) satisfies $0 \leq J(m/e)$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ on positive reals (equivalently $(x-1)^2/(2x)$). Nonnegativity of $J$ is the AM-GM inequality: $J(x)\ge 0$ whenever $x>0$, with equality only at $x=1$.
This module is Foundation RS Module 2: the eight-tick recognition epoch of period $2^D=2^3=8$, forced by spatial dimension $D=3$. Domain cost is the local specialization of $J$ to a positive mass-energy ratio $m/e$, so the same lower bound applies once positivity of the ratio is secured.
Upstream, Jcost_nonneg records exactly that bound (via the squared form or the $x+x^{-1}\ge 2$ rearrangement).
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio $m/e$). Positivity of $m/e$ follows from div_pos on the two strict positivity hypotheses. Feed that into the upstream lemma that $J(x)\ge 0$ for every $x>0$.
why it matters
Keeps every mass-energy domain cost inside the nonnegative cone required by the Recognition Composition Law and the forcing chain. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and sits in the eight-tick / $D=3$ layer (T7-T8 of the unified forcing chain). No downstream consumers are recorded yet; the lemma is infrastructure for later threshold and certificate constructions in the same module (canonical threshold positivity, the RS forcing-chain certificate).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.