domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the Recognition domain cost is nonnegative. Cosmology certificates that treat domain cost as a physical penalty cite this bound before comparing to the ISM dust fraction. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le C_{\mathrm{dom}}(m,e)$. (Here domain cost is the J-cost of the ratio $m/e$.)
background
Recognition Science measures multiplicative mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Upstream lemmas record that $J(x)\ge 0$ for every $x>0$, by AM-GM or by rewriting $J(x)=(x-1)^2/(2x)$.
This file is Cosmology RS Module 11, whose structural claim is that $J(\phi)^2\approx 1.39%$ matches the empirical $\sim 1%$ ISM dust fraction. Locally, domain cost on a mass-energy pair is the J-cost evaluated at their ratio. Nonnegativity is the elementary positivity fact needed before that cost can be used as a penalty in the certificate stack.
The module is marked structural (zero sorry, zero axiom). Constants and the Cost library supply $\phi$ and $J$; the present lemma only needs the positive-ratio case of J-nonnegativity.
proof idea
One-line wrapper. Unfold domain cost (definitionally $J(m/e)$), obtain $m/e>0$ from the two positivity hypotheses via div_pos, and finish by the upstream lemma that $J(x)\ge 0$ whenever $x>0$. No further algebraic work.
why it matters
Keeps domain cost admissible as a physical cost in the Module 11 ISM-dust certificate: a signed or negative cost would break the comparison $J(\phi)^2\sim 1%$ to the observed dust fraction. The module status is STRUCTURAL THEOREM; this lemma is the positivity hinge under that certificate (RSCosmo011Cert and siblings). It sits downstream of the Cost-library J-nonnegativity facts that also appear in the forcing chain (T5 J-uniqueness) and in gravity coherence bridges. No further used-by edges are recorded yet; the immediate consumer is the local cosmology certificate rather than a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.