domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost built from the J-cost of their ratio is non-negative. Collapse-threshold and GRW-rate arguments in the wavefunction-collapse-from-J-cost module rely on this sign fact. The proof is a one-line unfold of the domain cost followed by the standard J-cost non-negativity lemma on the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of mass $m$ and energy $e$ (the $J$-cost of the ratio $m/e$) satisfies $0 \le J(m/e)$.
background
The ambient module derives an objective (GRW-style) wavefunction collapse threshold from the Recognition Science J-cost. Status is structural: zero sorry, zero axioms. The target rate formula is $\lambda = J(\varphi)/(m_{\mathrm{nucleon}}\varphi^{20})$, compared numerically to the empirical $10^{-16},\mathrm{s}^{-1}$ scale; the module records a large structural mismatch and keeps the algebra clean.
The J-cost is the unique nonnegative cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $(x-1)^2/(2x)$. Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by AM-GM or by rewriting as a square over a positive denominator.
Here the domain cost of a positive mass $m$ and positive energy $e$ is exactly that J-cost evaluated at the ratio $m/e$. Non-negativity of the domain cost is therefore the specialization of J-nonnegativity to positive ratios.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes non-negativity of $J(m/e)$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge the goal by the upstream lemma that $J(x)\ge 0$ for every positive real $x$.
why it matters
Keeps every subsequent inequality about domain cost inside the collapse-from-J-cost development on the nonnegative side of the ledger. The module is the structural (not numerical) half of the GRW-style collapse rate built from $J(\varphi)$ and the $\varphi$-ladder mass scale; without domain-cost non-negativity, threshold comparisons and certificate constructions in the same file would not typecheck as order facts.
No downstream consumers are recorded yet in the graph, so this is a local hygiene lemma for the collapse certificate stack (canonical threshold positivity, WFCollapse3Cert, inhabited certificates). It sits under the broader T5 J-uniqueness landmark: once $J$ is forced, its sign is free and must be recorded before rates or thresholds are compared. The module itself flags that the numerical GRW match is off by many orders; this lemma does not close that gap, it only secures the sign algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.