domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Anyone building RS domain thresholds or fine-structure certificates cites this positivity gate. The proof is a one-line unfold of domain cost to the J-cost of the mass-to-energy ratio, then the standard AM-GM nonnegativity of J.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \leq J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition cost on the positive reals.
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 and the Recognition Composition Law. Upstream lemmas record $J(x)\ge 0$ 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 the J-cost of their ratio: $\mathrm{domainCost}(m,e)=J(m/e)$. The local setting is Physics RS Module 2, a structural (zero-sorry) package whose headline claim is that the RS fine-structure window places $\alpha^{-1}$ inside $(137.030,137.039)$, containing the CODATA value.
proof idea
One-line wrapper. Unfold the definition of domain cost 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 gate that keeps RS domain thresholds and certificate bundles well-defined on the physical orthant. The module packages EM fine-structure structure theorems (alpha band containing CODATA) as a zero-sorry structural certificate; this lemma supplies the cost nonnegativity used by sibling threshold and certificate declarations (canonicalThreshold_pos, RSPhysics002Cert). It sits downstream of the T5 J-uniqueness landmark and the Cost library's AM-GM form of $J\ge 0$. No further used-by edges are recorded yet; the result is infrastructure rather than a headline physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.