domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Foundation-layer arguments that treat domain cost as a genuine cost functional cite this bound. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \leq C_{\mathrm{dom}}(m,e)$. Equivalently, writing $C_{\mathrm{dom}}(m,e)=J(m/e)$ with the standard Recognition cost $J(x)=(x+x^{-1})/2-1$, one has $J(m/e)\ge 0$.
background
The ambient module is Foundation RS Structural Module 6, whose stated subject is phi uniqueness via the self-similar fixed point $\varphi=1+1/(1+1/(1+\cdots))$, recorded as a structural theorem with no sorry and no axioms.
Domain cost is the local cost functional on a positive mass–energy pair $(m,e)$. From its unfolding it equals the standard J-cost of the ratio: $C_{\mathrm{dom}}(m,e)=J(m/e)$. The J-cost itself is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain.
Upstream, Jcost_nonneg records that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM / $(x-1)^2/(2x)$).
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity witness into the upstream lemma Jcost_nonneg, which closes the goal.
why it matters
Nonnegativity is the minimal sanity check that domain cost behaves as a cost rather than a signed defect. The module packages structural facts around the forced golden ratio $\varphi$ (T6 of the forcing chain: the unique self-similar fixed point). Even though no downstream theorem currently lists this lemma as a direct dependency, it sits among the sibling certificates (RSFDNStructural006Cert, canonicalThreshold_pos) that underwrite the structural layer: costs must be nonnegative before thresholds, uniqueness, or ladder comparisons are meaningful. It inherits the AM-GM content of T5 J-uniqueness without reopening the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.