domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Gravity structural proofs that treat domain cost as J-cost on the mass-to-energy ratio cite this bound before comparing to thresholds. The argument is a one-line wrapper: unfold the definition and apply J-nonnegativity to the positive quotient.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le J(m/e)$, where domain cost is the J-cost of the mass-to-energy ratio.
background
Recognition Science measures structural mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). For $x>0$, $J(x)\ge 0$ by AM-GM, or by the identity $J(x)=(x-1)^2/(2x)$. That nonnegativity is recorded upstream as the standard J-cost lemma.
This file is Gravity RS Structural Module 5. Its setting is the RS eight-tick octave: period $2^D=8$, one complete traversal of the binary recognition lattice (forcing-chain landmark T7). Domain cost is the local packaging of J on a mass–energy ratio: for positive $m,e$, domain cost equals $J(m/e)$. Sibling declarations introduce a canonical threshold and a structural certificate that will consume such positivity facts.
proof idea
One-line wrapper. Unfold domain cost to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by positivity of division, so the upstream J-cost nonnegativity lemma applies directly and yields $0\le J(m/e)$.
why it matters
Positivity of domain cost is the minimal cost axiom needed before any threshold comparison in the gravity structural layer. The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and sits on the eight-tick lattice (T7, period $2^3=8$). Sibling material includes the canonical threshold, its positivity, and the RSGRVStructural005 certificate; those objects need domain cost to behave like a genuine nonnegative cost. No downstream uses are wired yet; the lemma closes a local obligation so later certificates can compare domain cost against thresholds without re-proving AM-GM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.