domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Physicists working the tree-level Weinberg angle or any RS cost bound in this module cite it as the basic positivity fact. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ satisfies $0\le\mathrm{domainCost}(m,e)$.
background
Physics RS Module 4 records the tree-level Weinberg angle identity $\sin^2\theta_W=J(\phi)/(1+J(\phi))\approx0.1054$ (loop-corrected to $\approx0.231$) as a structural theorem with no sorry and no axioms.
The underlying cost is the Recognition J-functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law. Upstream lemmas establish $J(x)\ge0$ for every $x>0$ by AM-GM (or by rewriting $J(x)=(x-1)^2/(2x)$). In this module the domain cost of a mass-energy pair is defined by evaluating that same $J$ on the positive ratio $m/e$.
proof idea
One-line wrapper. Unfold the definition of domain cost (which is $J$ of the ratio $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 nonnegativity.
why it matters
Positivity of every cost that appears in the Weinberg-angle module is a standing structural requirement of Recognition Science: the J-cost is the unique nonnegative generator compatible with the Recognition Composition Law and the T5 uniqueness theorem. This lemma discharges that obligation for the concrete domain-cost functional used here. No downstream theorems currently depend on it (used-by count is zero), so it functions as a local certificate rather than a bridge lemma; it still closes the nonnegativity gap that any later bound or comparison involving domain cost will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.