domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the RS domain cost is nonnegative. Landscape and vacuum-counting arguments that treat domain cost as a penalty cite this bound. The proof is a one-line wrapper: unfold the cost and apply nonnegativity of the J-cost at the positive ratio m/e.
Claim. If $m,e\in\mathbb{R}$ satisfy $m>0$ and $e>0$, then the domain cost of the pair $(m,e)$ is nonnegative: $0\le C_{\mathrm{dom}}(m,e)$.
background
The ambient module is a structural comparison of the string-theory vacuum landscape (~$10^{500}$ vacua) with Recognition Science counting built from powers of $\varphi$. Status is a fully discharged structural theorem (no sorry, no axioms).
Domain cost is the local cost assigned to a positive mass–energy pair $(m,e)$. From the proof shape it is the J-cost of the ratio $m/e$. The J-cost is the unique nonnegative cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$), which vanishes only at $x=1$.
Upstream, Jcost_nonneg records the elementary fact that $J(x)\ge 0$ whenever $x>0$, proved via the squared form $J(x)=(x-1)^2/(2x)$ or by AM-GM on $x+x^{-1}\ge 2$. That lemma is the only nontrivial input.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. Positivity of the ratio follows from div_pos on the two hypotheses $m>0$ and $e>0$. Discharge with the standard lemma that $J(x)\ge 0$ for every $x>0$.
why it matters
Keeps every domain-cost expression in the RS string-landscape module inside the nonnegative cone, so landscape penalties and threshold comparisons remain well-defined. No downstream consumers are wired yet in the graph; the immediate siblings are the domain-cost definition itself, equality-at-a-point lemmas, the canonical threshold and its positivity, and the landscape certificate.
In the forcing chain this rests on T5 (J-uniqueness): once $J$ is fixed as the unique cost obeying the Recognition Composition Law, nonnegativity is free and propagates to every derived cost, including domain cost. The module’s structural claim is that RS vacuum counting is $\varphi$-ladder based rather than a $10^{500}$-scale discrete landscape; a nonnegative domain cost is a prerequisite for any such comparison to be a genuine penalty rather than an indefinite score.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.