domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive pair $(m,e)$ is nonnegative: it is the J-cost of the ratio $m/e$. Cost and forcing-chain arguments cite this to keep inequalities oriented. The proof is a one-line unfold of the definition, then the standard nonnegativity of $J$ on positive reals.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost evaluated at the ratio $m/e$.
background
Recognition Science measures mismatch by the J-cost on positive reals, $J(x)=\frac{x+x^{-1}}{2}-1$, equivalently $J(x)=\frac{(x-1)^2}{2x}$. Upstream lemmas record $J(x)\ge 0$ for every $x>0$ (AM-GM / squared form), with equality only at $x=1$.
This file is Foundation RS Module 5: structural theorems of the forcing chain T0–T8, all proved in Lean with zero sorry. Domain cost is the specialization of $J$ to a two-argument ratio: after unfolding, it is exactly $J(m/e)$. The local hypotheses $m>0$ and $e>0$ place that ratio in the domain where J-nonnegativity applies.
proof idea
One-line wrapper. Unfold the domain-cost definition to expose $J(m/e)$. From $m>0$ and $e>0$, div_pos yields $m/e>0$. Apply the upstream lemma Jcost_nonneg (AM-GM form of $J\ge 0$ on positive reals) to that quotient.
why it matters
Module 5 packages the RS forcing chain T0–T8 as structural theorems with no sorry. Nonnegativity of domain cost is the elementary positivity gate for any later comparison of that cost against thresholds (siblings include a canonical threshold and its positivity certificate). It inherits the sign property forced by T5 J-uniqueness once the cost is specialized to a mass/energy-style ratio. The dependency graph lists no downstream users yet; the lemma is infrastructure for oriented cost inequalities inside the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.