domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass-energy pair is nonnegative. Cosmology and gap-45 structural arguments cite this to keep the RS cost on the correct side of zero when comparing mass and energy scales. Proof is a one-line unfold of the domain-cost definition, then the standard J-cost nonnegativity lemma on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le \mathrm{domainCost}(m,e)$. Under the module definition this is $0 \le J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition cost.
background
Recognition Science measures scale mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$, forced unique at T5 of the unified forcing chain and written equivalently as $\cosh(\log x)-1$. On positives it is nonnegative by AM-GM (equivalently, $J(x)=(x-1)^2/(2x)$).
This module is Cosmology RS Structural Module 4. It packages the gap-45 identity $D^2(D+2)=9\cdot5=45$ as the minimum rung for stable self-reference at $D=3$. Domain cost is the local cost assigned to a mass-energy pair: J applied to the ratio $m/e$.
Upstream nonnegativity of J on positive reals is already proved in the Cost library (and re-exported in related gravity modules), via the square form or the bound $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold the definition of domain cost, which is J of the ratio $m/e$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by positivity of division. Feed that positive quotient to the standard J-cost nonnegativity lemma.
why it matters
Keeps domain cost a genuine cost functional inside the gap-45 structural package: at $D=3$ (forced by T8) the combination $D^2(D+2)=45$ is the minimum rung for stable self-reference. Without nonnegativity, threshold comparisons against the module's canonical threshold would not be well-posed as cost inequalities.
The declaration is infrastructure for the module certificate and sibling positivity facts (canonical threshold positivity, the inhabited certificate). The dependency graph currently lists no downstream consumers, so it is a local positivity brick rather than a cited parent theorem. It does not itself prove gap-45; it only secures the sign of the cost used around that structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.