domainCost_nonneg
plain-language theorem explainer
For positive mass and energy scales, the cosmological domain cost is nonnegative. Cosmology and CMB-anisotropy arguments that treat domain cost as a J-cost on a positive ratio cite this bound. The proof is a one-line unfold of the definition followed by the standard nonnegativity of J on positive reals.
Claim. If $m>0$ and $e>0$ are real, then the domain cost of the pair $(m,e)$ satisfies $0 \le J(m/e)$, where $J$ is the Recognition J-cost $J(x)=(x+x^{-1})/2-1$.
background
The ambient module develops CMB anisotropy from J-cost (structural, zero sorry). The RS estimate is $J(\varphi)^{D+1}=J(\varphi)^4\approx 1.94\times 10^{-4}$, compared with the observed $\Delta T/T\sim 10^{-5}$ order of magnitude; here $D=3$ is the forced spatial dimension from the forcing chain.
Domain cost is the local cost assigned to a positive mass-energy ratio: after unfolding it is exactly $J(m/e)$. The J-cost itself is the unique nonnegative generator of the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced at T5.
Upstream, Jcost_nonneg records that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as a square (AM-GM / $(x-1)^2/(2x)$).
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. Positivity of the ratio $m/e$ is immediate from $m>0$ and $e>0$ via div_pos. Discharge the goal by the standard lemma that $J$ is nonnegative on positive reals.
why it matters
Keeps every domain-cost comparison in the MatterPert4 cosmology stack inside the nonnegative cone, so thresholds and certificates built on domain cost cannot go negative by algebraic accident. The module status line frames this as part of the structural CMB-anisotropy package: $J(\varphi)^4$ as the RS-side $\Delta T/T$ scale under $D=3$ (T8) and the unique J from T5.
No downstream dependents are recorded yet; the lemma is local hygiene for the sibling definitions (domainCost, canonicalThreshold, MatterPert4Cert). It does not itself produce the $10^{-5}$ amplitude, only the sign of the cost that those constructions consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.