domainCost_nonneg
plain-language theorem explainer
For positive mass and energy scales m and e, the domain recognition cost is nonnegative. Anyone bounding recognition costs or thresholds in the structural foundation layer would cite this. The proof is a one-line unfold of the domain cost into J-cost of the ratio m/e, then the standard J-nonnegativity lemma.
Claim. If $m>0$ and $e>0$, then the domain recognition cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Equivalently, writing the cost as the J-cost of the ratio, $0 \le J(m/e)$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ on positive reals. By AM-GM (or the squared form $(x-1)^2/(2x)$), $J(x)\ge 0$ whenever $x>0$, with equality only at $x=1$. The module records the structural fact that recognition cost is ratio-symmetric: $J(x)=J(1/x)$.
Domain cost packages that J-cost on a mass-to-energy ratio: for positive $m,e$ one sets $C_{\mathrm{dom}}(m,e):=J(m/e)$. The local setting is Foundation structural module 7 (zero sorry, zero axiom), which isolates elementary positivity and symmetry properties of this cost before they are used in thresholds and certificates.
Upstream, Jcost_nonneg already states $J(x)\ge 0$ for $x>0$, proved either by rewriting to a square over a positive denominator or by the elementary inequality $x+x^{-1}\ge 2$.
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. Apply the standard lemma that $J$ is nonnegative on the positive reals.
why it matters
Nonnegativity of domain cost is the first structural sanity check in RS_FDN_Structural_007: costs used as thresholds or certificate bounds must sit in $[0,\infty)$. It sits under the J-uniqueness landmark (T5): once $J$ is forced as the unique cost compatible with the Recognition Composition Law, every derived cost (including domain cost on ratios) inherits $J\ge 0$.
The module pairs this with ratio symmetry $J(x)=J(1/x)$, so domain cost depends only on the dimensionless ratio and is blind to overall scale. Downstream siblings (canonical threshold positivity, the structural certificate) rely on a nonnegative cost floor; without this lemma those certificates would not even type-check as real inequalities. No open sorry is involved; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.