domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Cosmology structural certificates use this to keep Recognition costs on mass-to-energy ratios from going negative. The argument is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive quotient.
Claim. For all reals $m>0$ and $e>0$, the domain cost of the pair is nonnegative: $0\le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
This sits in Cosmology RS Structural Module 10, whose calibration fixes the coherence energy $E_{\mathrm{coh}}$ once from the electron mass so that subsequent predictions are parameter-free. The module is marked structural (zero sorry, zero axiom).
Domain cost is the Recognition cost evaluated on the mass-to-energy ratio: after unfolding, $\mathrm{domainCost}(m,e)=J(m/e)$. The cost functional is the unique $J$ forced by the Recognition Composition Law, equivalently $J(x)=\cosh(\log x)-1$, and is nonnegative on $(0,\infty)$ by AM-GM.
Upstream, Jcost_nonneg states exactly that: for $x>0$, $J(x)\ge 0$, proved by rewriting $J$ as a square over a positive denominator (or by the elementary inequality $x+x^{-1}\ge 2$).
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 div_pos. Feed that positivity witness into the standard lemma that $J$ is nonnegative on positive reals, and finish.
why it matters
Nonnegativity of domain cost is a basic structural sanity check inside the RS cosmology stack: costs that can go negative would break the variational reading of mass–energy ratios and the parameter-free calibration story of Module 10. It rests on the same $J\ge 0$ fact that appears throughout the forcing chain (T5 J-uniqueness and the RCL). No downstream consumers are wired yet in the graph; the lemma is available for any certificate that needs a nonnegative cost on a positive mass-to-energy ratio, including the module’s own structural certificate bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.