domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the recognition domain cost is nonnegative. Cosmology and structural RS arguments cite this to treat domain costs as legitimate nonnegative cost functionals. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive mass-to-energy ratio.
Claim. For all real numbers $m>0$ and $e>0$, the recognition domain cost of the pair $(m,e)$ is nonnegative: $0\le C_{\mathrm{dom}}(m,e)$.
background
This module records structural facts about Recognition Science J-cost symmetry in a cosmology setting: the cost is ratio-symmetric, $J(x)=J(1/x)$, and the status is a fully proved structural theorem (no sorry, no axioms).
The underlying cost is the standard RS J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), defined for positive reals. Upstream, $J(x)\ge 0$ for $x>0$ is the AM-GM form of J-cost nonnegativity: after rewriting $J(x)=(x-1)^2/(2x)$, nonnegativity is immediate. Domain cost is the specialization of that cost to a positive mass-energy ratio (the definition unfolds to $J(m/e)$).
The local setting is therefore pure cost algebra on positive reals, not a dynamical cosmological model.
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 positivity of division, so the upstream lemma $J\ge 0$ on positive arguments applies directly and finishes the goal.
why it matters
Nonnegativity is the first structural sanity check for any RS cost used in cosmology: domain constructions must not produce negative recognition cost. The module frames this under J-cost ratio symmetry $J(x)=J(1/x)$, which is the algebraic content of the Recognition Composition Law specialization to reciprocal arguments and sits next to the T5 J-uniqueness landmark $J(x)=(x+x^{-1})/2-1$.
Sibling certificates in the same file (the structural 007 certificate and its inhabited instance) package this fact with related threshold positivity. Even with no recorded downstream dependents yet, the lemma closes the nonnegativity obligation for any later argument that treats domain cost as a cost functional on mass-energy pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.