domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is non-negative. Structural and gravity modules that bound recognition costs on mass-energy ratios cite this. The proof is a one-line unfold of the domain cost into J-cost of the ratio, then the standard AM-GM non-negativity of J on positive reals.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is non-negative: $0\le J(m/e)$, where $J$ is the Recognition J-cost.
background
The Recognition J-cost on positive reals is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). 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).
This module is Foundation RS Structural Module 5: the eight-tick octave (period $2^D=8$), one full traversal of the binary recognition lattice, marked as a structural theorem block with zero sorry and zero axioms.
Here the domain cost of a mass-energy pair is the J-cost of their ratio. Positivity of both arguments guarantees the ratio is positive, so the upstream non-negativity lemma applies directly.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(m/e)$. Feed the positive quotient (from div_pos on the two positivity hypotheses) into the upstream lemma that $J(x)\ge 0$ for $x>0$. No further algebraic work.
why it matters
Closes the elementary non-negativity obligation for domain costs inside the eight-tick structural layer (T7: period $2^3=8$). The sibling certificate RSFDNStructural005Cert packages this with the related threshold positivity facts; without non-negativity, cost comparisons and collapse thresholds in the foundation stack are ill-posed.
No downstream theorem edges are recorded yet, so the lemma currently serves as local hygiene for the structural certificate rather than a named step in a larger forcing chain. It inherits the T5 J-uniqueness background: the same $J$ forced by the Recognition Composition Law is the cost being bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.