domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Cited by anyone using the RS summary certificate or comparing domain-level costs to thresholds. Proof is a one-line unfold of the domain-cost definition, then nonnegativity of J on the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. Equivalently, if $C_{\mathrm{dom}}(m,e)=J(m/e)$ with $J(x)=(x+x^{-1})/2-1$, then $J(m/e)\ge 0$.
background
Recognition Science takes the cost $J(x)=(x+x^{-1})/2-1$ on $x>0$ as the unique functional forced by the Recognition Composition Law and the four foundation axioms (forcing step T5). By AM-GM, or by the identity $J(x)=(x-1)^2/(2x)$, one has $J(x)\ge 0$ with equality only at $x=1$.
This module is the structural summary certificate for Plan v7: one equation, phi forced, gap-45 forced, $D=3$ forced, constants derived, zero sorry and zero axioms. Domain cost is the same $J$ evaluated on a positive scale ratio of two domain quantities (here mass and energy parameters $m,e$). Upstream lemmas record $J\ge 0$ on positives in Cost and in related gravity bridges.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J$ at $m/e$), obtain $m/e>0$ from $m>0$ and $e>0$ via positivity of division, then apply the standard lemma that $J(x)\ge 0$ for $x>0$.
why it matters
Basic certificate hygiene inside Foundation.RecognitionScienceSummary3: any cost used against a canonical threshold must be known nonnegative. The sibling cluster (domain cost, equality-at-definition, canonical threshold positivity, and the inhabited summary cert) packages the claim that the uniquely forced $J$ behaves as a genuine cost. That nonnegativity is the content of T5-adjacent infrastructure in the forcing chain and is presupposed wherever RS compares costs to the Berry threshold or rung gaps. The dependency graph currently lists no downstream users; the lemma closes a local obligation rather than a multi-module bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.