domainCost_nonneg
plain-language theorem explainer
For positive reals m and e, the domain cost of the ratio m/e is nonnegative. Anyone building the RS quantum-error threshold (p_th ≈ 1.18%) cites this as the basic positivity fact on the cost that enters the threshold. The proof is a one-line unfold of domainCost followed by the standard J-cost nonnegativity lemma on the positive quotient.
Claim. If $m>0$ and $e>0$ are real, then the domain cost of the pair $(m,e)$ satisfies $0 \le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
The module fixes the RS prediction for the quantum-error-correction fault-tolerance threshold: $p_{\mathrm{th}}=J(\varphi)/10\approx 1.18%$, compared with surface-code and color-code empirics near 1.0–1.1%. Status is structural (no sorry, no axioms).
Domain cost is the local cost functional on a mass/energy pair: after unfolding it is simply $J(m/e)$. The Recognition cost $J$ is the unique nonnegative generator forced by the Recognition Composition Law (T5); equivalently $J(x)=\cosh(\log x)-1$, and $J(x)\ge 0$ for all $x>0$ by AM-GM.
Upstream, Jcost_nonneg records exactly that inequality: for $x>0$, $0\le J(x)$, proved either by rewriting $J$ as a square over a positive denominator or by the elementary bound $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity witness into the upstream lemma Jcost_nonneg and finish.
why it matters
Positivity of domain cost is the first structural sanity check inside the RS quantum-error-rate development. The module’s headline claim is the exact threshold $p_{\mathrm{th}}=J(\varphi)/10$; every later comparison with surface-code and color-code numbers presupposes that the underlying cost cannot go negative. The result sits on the T5 uniqueness of $J$ and on the global nonnegativity of the cost that appears throughout the forcing chain. No downstream theorems are recorded yet; the lemma is infrastructure for the threshold certificate and the inhabited certificate object in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.