domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass–energy pair is nonnegative. Collapse and ledger-posting arguments in the RS wave-function module cite this to keep the cost functional well-posed before threshold comparisons. The proof is a one-line unfold reducing to nonnegativity of the J-cost on the ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le \mathrm{cost}(m,e)$, where that cost is the J-cost of the positive ratio $m/e$.
background
The module treats wave-function collapse as a recognition event: measurement equals ledger posting. Collapse is framed as J-cost minimization onto the nearest rung of the phi-ladder; the eight-tick cycle sets the minimal recognition time. No hidden variables are invoked.
The J-cost is the standard RS cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), defined for $x>0$. Upstream, $J(x)\ge 0$ on positives is the AM-GM form of the cost (Cost.Jcost_nonneg and parallel Gravity copies). Domain cost is the local specialization of that cost to a mass–energy pair: it unfolds to $J(m/e)$. The positivity hypotheses on $m$ and $e$ guarantee the ratio lies in the domain of $J$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The ratio $m/e$ is positive by div_pos from $m>0$ and $e>0$. Discharge with the upstream lemma Jcost_nonneg (AM-GM / square form of $J$).
why it matters
Keeps the cost side of the RS collapse story mathematically clean: every later comparison against a canonical threshold or certificate of collapse needs a nonnegative ledger cost. The module status is structural theorem (zero sorry, zero axiom); this lemma is the elementary nonnegativity brick under that claim.
It sits next to siblings that define domain cost, evaluate it at equality cases, and build the collapse certificate (RSWFCollapseCert, cert, cert_inhabited). Framework landmark: T5 J-uniqueness fixes the cost shape whose nonnegativity is used here; collapse-as-minimization is the module’s reading of measurement. No downstream theorems currently depend on it in the graph, so its role is local hygiene inside the collapse certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.