domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Physicists tracking the proton-electron mass-ratio scaffolding in RS Physics Module 9 cite this as a basic positivity guard. The proof is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \leq C_{\mathrm{dom}}(m,e)$.
background
RS Physics Module 9 is a structural (zero-sorry) package aimed at the proton-electron mass ratio. The raw phi-ladder estimate $\phi^{12}\approx 321.9$ sits a factor $\sim 5.7$ below the observed $\approx 1836$, so the module records positivity and threshold lemmas that any later correction term must respect.
The underlying cost is the Recognition J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and nonnegative on $(0,\infty)$ by AM-GM. Domain cost is the specialization of $J$ to the positive ratio $m/e$; the present lemma simply records that specialization inherits nonnegativity.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio $m/e$), obtain positivity of the ratio from div_pos on the two strict inequalities $m>0$ and $e>0$, then apply the upstream lemma Jcost_nonneg (AM-GM form of $J\ge 0$ on positive reals).
why it matters
Module 9 is labeled STRUCTURAL THEOREM and sits in the physics layer that will eventually close the proton-electron mass gap on the phi-ladder. Nonnegativity of domain cost is the minimal sanity check before any threshold or certificate (canonicalThreshold, RSPhysics009Cert) can be stated. No downstream consumers are wired yet (used_by empty), so the lemma presently anchors the local certificate rather than feeding a named parent theorem. It inherits the T5 uniqueness of $J$ and the global nonnegativity already proved in Cost and Gravity bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.