domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Citation targets are lower bounds on recognition imbalance between two positive scales, and any certificate that needs J ≥ 0 on a ratio. The argument is a one-line unfold of domain cost into ordinary J-cost on m/e, then the AM-GM nonnegativity lemma.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$, so the claim is $J(m/e)\ge 0$.
background
Module 4 of the Foundation RS forcing chain records structural facts about the J-cost: its unique minimum $J(1)=0$ at unit ratio (equilibrium), and the value $J(\varphi)=\varphi-3/2$ at the golden ratio. Status is structural theorem (no sorry, no axiom).
The J-cost is the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg states that $J(x)\ge 0$ for every positive $x$, proved by rewriting $J$ as a square over a positive denominator (AM-GM). Domain cost is the specialization of that cost to a mass–energy ratio: after unfold, $C_{\mathrm{dom}}(m,e)=J(m/e)$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. Positivity of the ratio follows from div_pos on the two hypotheses $m>0$ and $e>0$. Discharge the goal by the upstream lemma that $J(x)\ge 0$ whenever $x>0$.
why it matters
Nonnegativity of domain cost is the first structural guard in Module 4: cost cannot go negative on any admissible mass–energy pair, so the equilibrium $J(1)=0$ is a true global minimum rather than a local dip. That fact sits under the T5 J-uniqueness landmark in the forcing chain and under the Recognition Composition Law that forces the explicit form of $J$.
No external used_by edges are recorded; the lemma is consumed inside the module’s own certificate (RSForcingChain004Cert and the inhabited cert witness). It therefore closes a local obligation rather than a cross-module bridge, but without it the module’s claim that J is a genuine cost on domain ratios would be incomplete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.