domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Anyone placing lower bounds on recognition cost over the mass-energy plane cites this fact. The argument is a one-line wrapper: unfold the definition and invoke nonnegativity of the J-cost on the positive ratio.
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)$. Equivalently, writing the cost as the J-cost of the ratio, $0\le J(m/e)$.
background
The J-cost on positive reals is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream lemmas record $J(x)\ge 0$ for $x>0$ by AM-GM (or by rewriting $J(x)=(x-1)^2/(2x)$ and positivity). That nonnegativity is the only external input here.
In this module the domain cost of a pair $(m,e)$ is the J-cost of their ratio: $C_{\mathrm{dom}}(m,e):=J(m/e)$. The local setting is Structural Module 5 of the Recognition Mathematics layer, whose header fixes the eight-tick period $2^D=8$ (one full traversal of the binary recognition lattice) and marks the file as a structural theorem block with zero sorry and zero axioms.
proof idea
One-line wrapper. Unfold the definition of domain cost, which exposes $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity witness into the upstream lemma Jcost_nonneg, which returns $0\le J(m/e)$.
why it matters
Nonnegativity of domain cost is the elementary positivity gate for any later comparison of recognition cost against a canonical threshold on the mass-energy plane (siblings include canonicalThreshold and its positivity). In the Recognition forcing chain this sits under the T5 uniqueness of $J$ and the T7 eight-tick octave that the module header records. No downstream theorems currently depend on it in the graph, so it functions as a reusable structural lemma rather than a step inside a larger named certificate. It closes no open scaffold; it simply makes the cost functional safe to use as a lower bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.