domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Structural and gravity modules that treat recognition cost as a barrier or Lyapunov quantity cite this fact. The argument is a one-line wrapper: unfold the domain-cost definition to the J-cost of the positive ratio, then apply the standard J-cost nonnegativity lemma.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$.
background
The ambient module is Foundation RS Structural Module 3, which records the RS count law $2^D-1=7$ independent channels forced by configuration dimension $D=3$. Status is structural: zero sorry, zero axioms.
Domain cost is the local cost functional on a positive mass-energy pair. From the proof shape it is the J-cost of the ratio $m/e$. The J-cost is the Recognition Science cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law.
Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM / positivity). Several gravity bridges restate the same nonnegativity for local use.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the upstream lemma that $J(x)\ge 0$ for every positive real $x$.
why it matters
Nonnegativity of domain cost is the elementary positivity fact needed before any comparison of domain cost against a canonical threshold, or before treating cost as a barrier in structural channel counting. The module frames the RS count law ($2^D-1=7$ channels from $D=3$), which sits on the forcing-chain landmarks T7 (eight-tick octave) and T8 ($D=3$). No downstream consumers are wired yet in the graph; the lemma still closes the positivity side of the structural certificate for this module. It does not itself force the channel count; it only guarantees the cost side is well-behaved on the positive orthant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.