domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Researchers bounding costs inside the D=3 configuration-dimension argument cite this fact. The proof is a one-line wrapper: unfold the domain cost to the J-cost of the mass-to-energy ratio and invoke nonnegativity of J on positive reals.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. Equivalently, if $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$, then $J(m/e)\ge 0$.
background
The ambient module forces spatial dimension $D=3$ from eight-tick closure: the recognition cycle has period $8=2^3$, so exactly three binary recursions close the lattice; that is the unique minimal self-similar dimension (T8 in the forcing chain).
The underlying cost is the recognition functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Upstream lemmas record that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM). Domain cost is the specialization of $J$ to the positive ratio of a mass parameter to an energy parameter; the present statement simply inherits nonnegativity from that specialization.
proof idea
One-line wrapper. Unfold the definition of domain cost, which exposes $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity witness into the standard lemma Jcost_nonneg, which returns $0\le J(m/e)$.
why it matters
Nonnegativity of domain cost is a local positivity lemma inside the structural certificate that $D=3$ is forced by eight-tick closure. The module is marked zero-sorry and zero-axiom; this fact keeps every cost comparison inside that certificate well-defined and ordered. It sits beside the siblings that define the cost, evaluate it at equality cases, and package the full ConfigDimD3_v3Cert. Framework landmark: T8 (three spatial dimensions from period $2^3$). No downstream theorems are currently wired, so the lemma is infrastructure rather than a cited bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.