domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Structural and gravity-side arguments that treat domain cost as a J-cost on a ratio cite this bound before comparing to thresholds. The proof is a one-line unfold of the definition followed by the standard J-cost nonnegativity lemma on the positive quotient.
Claim. Let $m,e\in\mathbb{R}$ with $m>0$ and $e>0$. Then the domain cost of the pair satisfies $0\le \mathrm{domainCost}(m,e)$. Equivalently, writing the cost as the Recognition J-cost of the ratio, $0\le J(m/e)$.
background
This module is Foundation RS Structural Module 2: it records structural facts about the Recognition J-cost, including the golden-ratio minimum $J(\varphi)=\varphi-3/2\approx 0.11803$. Status is fully proved (no sorry, no axioms).
The Recognition cost is $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$, or $(x-1)^2/(2x)$). Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by rewriting to a square over a positive denominator (AM-GM / positivity).
Here domain cost is the local wrapper that feeds a positive mass-energy pair into that cost: after unfolding, $\mathrm{domainCost}(m,e)=J(m/e)$. The hypotheses $m>0$ and $e>0$ guarantee the ratio is positive, so the Cost-layer lemma applies directly.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The quotient $m/e$ is positive by div_pos on the two strict positivity hypotheses. Discharge with the upstream lemma Jcost_nonneg from IndisputableMonolith.Cost (AM-GM / square form of $J$). No further case splits or algebraic work.
why it matters
Nonnegativity is the first structural sanity check on any cost used as a recognition defect: costs must sit above zero before one compares them to the golden-ratio floor $J(\varphi)$ or to canonical thresholds in this module. It sits in the same structural layer as the T5 J-uniqueness landmark ($J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law, which presuppose a nonnegative cost functional on positive reals.
The module packages related facts (domainCost_at_eq, canonicalThreshold_pos, and the RSFDNStructural002Cert certificate). No downstream dependents are wired yet in the graph; the lemma is infrastructure for later threshold and coherence comparisons rather than a step inside a named parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.