domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Cost and forcing-chain arguments that treat dimensionless ratios as J-inputs cite this bound. Proof is a one-line unfold of domain cost to J on the positive ratio m/e, then the standard J-nonnegativity lemma.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Here $C_{\mathrm{dom}}(m,e)=J(m/e)$ with the Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$) on positive reals.
background
Module 12 of the RS foundation chain records dimensionless identities around the golden ratio, including the exact evaluation $J(\varphi)=\varphi-3/2\approx 0.11803$, and is marked structural (no sorry, no axioms).
The Recognition cost $J$ is the unique nonnegative functional fixed by the Recognition Composition Law and the T5 uniqueness step: $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $(x-1)^2/(2x)$. Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by rewriting to a square over a positive denominator (AM-GM / positivity).
Domain cost is the local specialization of that cost to a positive mass–energy pair: it is $J$ evaluated on the dimensionless ratio $m/e$. Nonnegativity of domain cost is therefore the same positivity statement transported to that ratio.
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. Apply the upstream lemma that $J$ is nonnegative on every positive real.
why it matters
In the forcing chain, T5 fixes $J$ as the unique cost; every later quantitative bound (thresholds, coherence collapse, energy-processing bridges) needs $J\ge 0$ on the ratios that appear. This lemma packages that fact for the mass–energy domain cost used in Module 12’s dimensionless bookkeeping around $J(\varphi)=\varphi-3/2$.
No downstream consumers are wired in the current graph, so the declaration is a local hygiene fact: it keeps domain-cost expressions inside the nonnegative cone before canonical thresholds and the Module-12 certificate are assembled. It does not itself force $\varphi$, the eight-tick period, or $D=3$; those sit elsewhere in T6–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.