domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Physicists tracking Recognition cost bounds in the top-Yukawa module cite this positivity fact before threshold or certificate arguments. The proof is a one-line wrapper: unfold domain cost to the J-cost of the mass-to-energy ratio and invoke the standard AM-GM nonnegativity of J.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
Recognition Science measures mismatch by the 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. Upstream lemmas record $J(x)\ge 0$ for every $x>0$ by AM-GM (or the squared form $(x-1)^2/(2x)$).
In this module the domain cost of a mass–energy pair is the J-cost of their ratio: after unfolding, $C_{\mathrm{dom}}(m,e)=J(m/e)$. The local setting is Physics RS Module 7 (top Yukawa $y_t=1$ at unification; the top quark sits at the $\phi^0=1$ coupling), marked as a structural theorem block with no sorry and no axioms.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg (AM-GM form from Cost, or the equivalent Gravity copies) to finish.
why it matters
Positivity of domain cost is the elementary sign check needed before any threshold, certificate, or comparison that treats mass–energy mismatch as a Recognition cost. The module frames the top quark as the $\phi^0=1$ Yukawa coupling at unification; a nonnegative cost on the mass–energy ratio keeps that structural story consistent with the global J-cost calculus (T5 uniqueness and the Recognition Composition Law). No downstream consumers are wired yet in the graph, so the lemma presently anchors the local certificate RSPhysics007Cert rather than a larger forcing step. It closes a trivial but mandatory nonnegativity obligation inside a zero-sorry physics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.