domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass-energy pair is nonnegative. Cost-functional arguments on ratio domains in Recognition Science cite this as the baseline sanity check. The proof is a one-line wrapper: unfold the definition and apply nonnegativity of J-cost to the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair 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)=\frac{x+x^{-1}}{2}-1$ on $x>0$. By AM-GM, $J(x)\ge 0$ with equality only at $x=1$. Equivalently, $J(x)=\frac{(x-1)^2}{2x}$. The module records structural facts about ratio-symmetric recognition cost: $J(x)=J(1/x)$.
Domain cost of a mass-energy pair is the J-cost of their ratio. Upstream, J-cost nonnegativity is proved by rewriting $J$ as a square over a positive denominator, or by the elementary bound $x+x^{-1}\ge 2$. Both routes require only $x>0$.
proof idea
One-line wrapper. Unfold domain cost (defined as J-cost of the ratio $m/e$), then apply the upstream nonnegativity lemma for J-cost to the positive quotient produced by div_pos from the two positivity hypotheses.
why it matters
Structural nonnegativity lemma in Mathematics RS Structural Module 7, which packages J-cost ratio symmetry as a zero-sorry structural theorem. Nonnegativity of domain cost is the baseline check that recognition cost never goes negative on physical mass-energy ratios. It sits under the T5 landmark: J is the unique cost satisfying the Recognition Composition Law with the standard normalization. No downstream dependents are recorded yet; the module certificate objects bundle this fact with the companion symmetry and threshold lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.