domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Cite when treating the RS cost on a mass-to-energy ratio as a genuine defect (thresholds, certificates in Physics Module 10). Proof is a one-line unfold of the domain-cost definition, then the standard nonnegativity of J on the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le C_{\mathrm{dom}}(m,e)$. Equivalently, if domain cost is $J(m/e)$ with $J(x)=(x+x^{-1})/2-1$, then $J(m/e)\ge 0$.
background
Physics RS Module 10 is the structural Higgs-mass match: $m_H\approx 125.25$ GeV against a $\varphi$-ladder rung ($\varphi^{13}$ scaled into GeV). Status is a structural theorem block (zero sorry, zero axiom).
The Recognition cost $J$ is the unique nonnegative defect off the fixed point $x=1$, $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $(x-1)^2/(2x)$). Domain cost packages that $J$ on a mass-to-energy ratio $m/e$.
Upstream, Jcost_nonneg states "$J(x)\ge 0$ for positive $x$ (AM-GM inequality)" and is proved by rewriting $J$ in squared form and applying positivity, or by the elementary bound $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold domain cost to expose $J$ of the ratio $m/e$. Feed div_pos hm he into Jcost_nonneg to obtain $0\le J(m/e)$. No further algebra.
why it matters
Local nonnegativity fact for the domain-cost functional inside the Higgs-mass physics module. It licenses treating domain cost as a true cost when comparing against canonical thresholds (siblings canonicalThreshold, canonicalThreshold_pos) and when assembling the module certificate RSPhysics010Cert.
Framework link: T5 forces uniqueness of $J$; nonnegativity is the companion structural property that makes $J$ a cost rather than a signed defect. The Recognition Composition Law and the $\varphi$-ladder mass formula sit downstream of that cost structure; this lemma keeps the Module-10 side consistent with them.
The dependency graph currently lists no external used_by edges, so the lemma is module-local infrastructure rather than a cross-cutting export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.