domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Spectrum and energy-ladder arguments in the Recognition foundation cite this as the basic positivity gate on the cost that feeds the discrete levels. The proof is a one-line wrapper: unfold the domain cost and apply J-cost nonnegativity to the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$.
background
The module builds the Recognition spectrum of $H_{RS}$ from the phi-ladder: levels $E_n = J(\varphi^n),\hbar_R,\omega_0$ for $n=0,1,2,\ldots$, with ground state $E_0=0$ and first excited state the recognition quantum $E_1=J(\varphi),\hbar_R,\omega_0$.
The J-cost is the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting as a square over a positive denominator (AM-GM).
Here the domain cost of a pair $(m,e)$ is the J-cost of their ratio. Positivity of that ratio is the only arithmetic needed before invoking the upstream nonnegativity lemma.
proof idea
One-line wrapper. Unfold domainCost so the goal is nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the upstream lemma Jcost_nonneg on that positive ratio.
why it matters
Positivity of the domain cost is the elementary gate that keeps spectrum energies on the nonnegative ray before the phi-ladder discretization is imposed. The module is marked structural (zero sorry, zero axiom) and sits in the Foundation layer that feeds the forcing chain landmarks: T5 J-uniqueness and T6 the self-similar fixed point $\varphi$. No downstream consumers are wired yet in the graph; the lemma is infrastructure for the nearby certificate RecogSpectrum3Cert and the canonical threshold siblings in the same file. It does not itself force the discrete spectrum, only the sign of the cost that multiplies $\hbar_R\omega_0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.