domainCost_nonneg
plain-language theorem explainer
For positive mass and energy scales the Recognition domain cost is nonnegative. Cosmology structural arguments cite this as a basic sanity bound on mass-energy ratios under the RS cost. The proof is a one-line wrapper: unfold the domain-cost definition and apply nonnegativity of J at the positive quotient.
Claim. For all real $m>0$ and $e>0$, the Recognition domain cost of the pair is nonnegative: $0\le J(m/e)$, where $J(x)=\frac12(x+x^{-1})-1$.
background
Recognition Science uses the cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), forced unique at T5 of the unified forcing chain. On $(0,\infty)$ one has $J\ge 0$ by AM-GM, or by rewriting $J(x)=(x-1)^2/(2x)$.
This module packages RS structural cosmology predictions: the forced form of $J$, $\varphi$ as the self-similar fixed point, and $D=3$. Status is structural theorem (zero sorry, zero axiom). The domain cost of a mass-energy pair $(m,e)$ is the cost of their ratio, $J(m/e)$.
Upstream nonnegativity lemmas state that $J(x)\ge 0$ whenever $x>0$, proved by the square form or by $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold the domain-cost definition so the goal is nonnegativity of $J$ at $m/e$. Positivity of the quotient follows from $m>0$ and $e>0$. Discharge by the standard lemma that $J(x)\ge 0$ for all $x>0$ (AM-GM / square form).
why it matters
Sits in the first RS cosmology structural module, which records the forced $J$, golden-ratio fixed point, and $D=3$ as a zero-sorry package. Nonnegativity of domain cost is a minimal physical constraint: mass-energy ratios cannot carry negative recognition cost under the T5 functional.
No downstream uses are wired in the graph yet. Sibling certificate objects in the same module collect this inequality with related structural facts (threshold positivity, inhabited cert). It does not itself force $\varphi$ or $D=3$; those are separate landmarks (T6, T8). It simply keeps the cost side of the cosmology interface nonnegative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.