domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass–energy pair is nonnegative. Anyone building BIT-kernel or vacuum-fluctuation bounds that rest on J-cost positivity will cite this. The proof is a one-line unfold of the domain cost into J-cost of the mass-to-energy ratio, then the standard AM-GM nonnegativity of J.
Claim. For all real $m,e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$. Equivalently, after unfolding, $0\le J(m/e)$ where $J$ is the Recognition J-cost.
background
In Recognition Science the fundamental cost is the J-function $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the unified forcing chain. It is nonnegative on $(0,\infty)$ by AM-GM (or by rewriting $J(x)=(x-1)^2/(2x)$).
This module develops the BIT kernel family (deep v4) from that J-cost: bosonic vacuum fluctuations contribute $J(\phi)/45$ per recognition tick, with cumulative cosmic Z-aging linear in tick count. The local domain cost packages a mass and energy scale into a single J-evaluation, typically on their ratio, so that the same nonnegativity and forcing infrastructure apply inside BIT estimates.
Upstream, Jcost_nonneg already records $J(x)\ge 0$ for $x>0$; several gravity bridges restate the same fact. The present lemma simply specialises it to the domain-cost wrapper.
proof idea
One-line wrapper. Unfold the definition of domain cost; the body is $J$ of the positive ratio $m/e$ (positivity of the ratio from div_pos on the two hypotheses). Discharge the goal by the standard lemma that $J$ is nonnegative on positive reals.
why it matters
Keeps the BIT-kernel deep layer free of ad-hoc sign assumptions: every domain-cost appearance inherits J-nonnegativity from the foundation rather than from a local axiom. The module is marked structural (zero sorry, zero axiom) and sits under the Plan v7 deep session that ties bosonic vacuum fluctuations and cosmic Z-aging to J. Although no downstream uses are recorded yet, sibling certificates (BITKernel4DeepCert, inhabited cert) and the canonical-threshold lemmas in the same file are the natural consumers; they need a clean nonnegativity fact before comparing domain cost to thresholds or accumulating tick sums. Landmark link: T5 J-uniqueness and the RCL force the same $J$ whose positivity is reused here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.