domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Horizon-problem arguments in the RS cosmology module rely on this to keep the cost functional on the admissible side of zero. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J-cost on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le \mathrm{cost}(m,e)$. Here domain cost is the J-cost of the ratio $m/e$, so the claim is $J(m/e)\ge 0$.
background
The module frames the cosmological horizon problem as a structural consequence of the eight-tick forcing chain and the J-cost. In Recognition Science the cost is $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), forced unique at T5 of the unified forcing chain; it vanishes only at $x=1$ and is nonnegative on $(0,\infty)$ by AM-GM.
Domain cost is that same $J$ evaluated on the mass-to-energy ratio $m/e$. The module doc states a structural theorem (zero sorry, zero axiom) resolving the horizon problem via $N_e=44$ e-folds at $T=J(\varphi),T_{\mathrm{Planck}}$, with expansion factor $\varphi^{44}\sim 10^9$, read as consistent with the usual $10^{24}$–$10^{26}$ requirement under the RS interpretation.
Upstream, J-cost nonnegativity is the standard lemma: for $x>0$, $J(x)\ge 0$, proved either from the squared identity $J(x)=(x-1)^2/(2x)$ or by rewriting $x+x^{-1}\ge 2$.
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 positivity of division, so the standard J-cost nonnegativity lemma applies directly and yields $0\le J(m/e)$.
why it matters
Keeps the cost accounting of causal domains nonnegative inside the horizon-problem certificate developed in this module (siblings include the certificate, its inhabited instance, and positivity of the canonical threshold). Nonnegativity is the minimal analytic hygiene needed before comparing domain costs across the $\varphi$-ladder expansion that the module invokes for $N_e=44$ e-folds.
Framework landmarks in play are T5 (J uniqueness), T6 ($\varphi$ as self-similar fixed point), and T7 (eight-tick octave), which together underwrite the temperature and expansion-factor claims in the module doc. No downstream uses are recorded yet; the lemma is local scaffolding for the structural horizon certificate rather than a global forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.