domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost is nonnegative. Physicists citing the RS cost layer in the strong-CP / eight-tick module use this as a basic positivity fact. The proof is a one-line wrapper: unfold the definition and apply J-cost nonnegativity to the positive mass-energy ratio.
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$ on positive reals. Upstream, Jcost_nonneg records $J(x)\ge 0$ for $x>0$, proved via the squared form $(x-1)^2/(2x)$ (AM-GM). Equality holds at $x=1$.
In this module the domain cost of a mass-energy pair is that same $J$ evaluated on the ratio $m/e$. The local setting is Physics RS Module 8: QCD $\theta=0$ forced by eight-tick uniqueness, presented as a structural theorem with no sorry and no axioms. Positivity of the domain cost is the elementary inequality needed before thresholds and certificates are stated.
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. Finish by applying the upstream lemma that $J(x)\ge 0$ for every positive $x$.
why it matters
Module 8 claims a structural solution of the strong CP problem: $\theta_{\mathrm{QCD}}=0$ from eight-tick uniqueness (primer landmark T7). Domain-cost nonnegativity is the first inequality in that cost layer; sibling declarations build the canonical threshold, its positivity, and the module certificate RSPhysics008Cert.
The result sits on T5 $J$-uniqueness: once $J$ is forced, every derived cost inherits nonnegativity for free. The dependency graph lists no further consumers yet, so this lemma is infrastructure for the certificate rather than a cited step in a longer chain. It closes no open scaffold; it simply makes the cost functional safe to use as a Lyapunov-style quantity on positive mass-energy pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.