domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Physicists tracking RS cost functionals in the W-boson mass module cite this as the basic positivity fact. The proof is a one-line wrapper: unfold the domain cost to the J-cost of the mass-to-energy ratio and apply J-cost nonnegativity.
Claim. For all real $m,e>0$, the domain cost satisfies $0\le J(m/e)$, where the domain cost is the Recognition J-cost of the mass-to-energy ratio.
background
Module 12 of the RS physics stack records the structural match of the W boson mass to a phi-ladder prediction ($M_W\approx 80.4,\mathrm{GeV}\sim\phi^{13}\cdot 0.154$). The local cost object is the domain cost of a positive mass $m$ and positive energy scale $e$.
That cost is the standard Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) evaluated at the ratio $x=m/e$. Upstream, $J(x)\ge 0$ for every $x>0$ is already proved by AM-GM (or by rewriting $J(x)=(x-1)^2/(2x)$ and positivity). The present lemma simply specializes that fact to the domain-cost definition.
proof idea
One-line wrapper. Unfold domainCost to expose $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos, so the upstream lemma Jcost_nonneg applies directly and yields $0\le J(m/e)$.
why it matters
Positivity of domain cost is the elementary sanity check that the cost functional used in the W-boson structural certificate cannot go negative. It sits beside the sibling facts domainCost_at_eq and canonicalThreshold_pos that feed the module certificate RSPhysics012Cert. In the broader forcing chain it inherits nonnegativity of the unique J forced at T5, so every later mass or threshold comparison built from domain cost starts from a genuine cost rather than a signed defect. No downstream theorem currently depends on it by name; it is infrastructure for the module's own certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.