domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Cosmology structural arguments cite this whenever a lower bound on that cost is needed. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of the J-cost to the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le J(m/e)$, where $J$ is the Recognition J-cost.
background
This module records structural cosmology facts forced by Recognition Science once spatial dimension is fixed at $D=3$. The headline count law is $2^D-1=7$ independent channels; the file is marked structural (zero sorry, zero axiom).
The J-cost is the unique cost functional forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg states that $J(x)\ge 0$ for every positive $x$, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
Here the domain cost of a positive pair $(m,e)$ is defined to be that same $J$ evaluated at the ratio $m/e$. Positivity of the ratio is immediate from the two positivity hypotheses, so the cost inherits nonnegativity from $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost, which exposes $J(m/e)$. The two strict positivity hypotheses give $m/e>0$ by div_pos. Feed that witness into the upstream lemma that $J(x)\ge 0$ for all $x>0$, and close.
why it matters
Nonnegativity is the first sanity check any Recognition cost must pass before it can bound cosmological thresholds or certify structural identities. In this file it sits beside the canonical threshold and the RS-COS structural certificate, so later cosmology lemmas can treat domain cost as a genuine nonnegative defect rather than an arbitrary real functional.
The result is local scaffolding for the $D=3$ count-law package ($2^D-1=7$ channels). It does not itself force dimension or the octave; those live in the T7/T8 forcing chain. No downstream dependents are recorded yet, so its present role is certificate hygiene inside the structural module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.