domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Cosmology arguments that treat solar-metallicity or other J-cost comparisons as a cost functional rely on this bound. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J on the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le J(m/e)$, where domain cost is the Recognition $J$-cost of the mass-to-energy ratio.
background
Module RS_Cosmo_Module_010 is the structural cosmology certificate for solar metallicity: $J(\varphi)^2\approx 0.01393$ matches $Z_\odot\approx 0.014$, with zero sorry and zero axioms. The local cost object is domain cost, defined by unfolding as the standard Recognition cost $J$ evaluated on the ratio $m/e$.
The Recognition cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law. Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM / positivity).
proof idea
One-line wrapper. Unfold domain cost to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity into the upstream lemma that $J$ is nonnegative on the positive reals, and finish.
why it matters
Keeps the cosmology cost layer honest: every domain-cost comparison used in the solar-metallicity match is a genuine nonnegative cost, not an ad-hoc signed residual. The module status is STRUCTURAL THEOREM; this lemma is the elementary nonnegativity gate for that certificate. No downstream consumers are wired yet in the graph, so it presently anchors the local cost API rather than a named parent theorem. It sits under the same $J$-cost infrastructure that appears in T5 J-uniqueness and in the broader Recognition cost calculus ($c=1$, $\hbar=\varphi^{-5}$, etc.).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.