domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass-energy pair is nonnegative. Workers on the D=3 recognition metric cite this to keep the J-cost Riemannian structure positive semidefinite on ratios. Proof is a one-line unfold of the domain-cost definition, then J-nonnegativity on the positive quotient.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair (the J-cost of the ratio $m/e$) is nonnegative: $0\le J(m/e)$.
background
The module fixes the D=3 configuration space $C_3=\mathbb{R}^3$ with the recognition metric $ds^2=J(dx/x)$ on the positive orthant, and records that this metric is positive definite for all $x>0$. Status is structural (zero sorry, zero axiom).
Domain cost is the packaging of J on a mass-to-energy ratio: after unfold it is exactly $J(m/e)$. The cost function itself is the unique T5 solution $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), with the squared form $J(x)=(x-1)^2/(2x)$.
Upstream, Jcost_nonneg states $J(x)\ge 0$ for every $x>0$, proved by AM-GM or by rewriting to a square over a positive denominator.
proof idea
One-line wrapper. Unfold domain cost to expose $J(m/e)$. Feed positivity of the quotient via div_pos on the two hypotheses $m>0$, $e>0$, then apply the upstream lemma that $J$ is nonnegative on positives.
why it matters
Local positivity lemma for the D=3 configuration-space story. Nonnegativity of domain cost is the elementary half of the claim that the recognition metric is positive semidefinite on the positive orthant; the module packages this into the structural certificate ConfigSpaceD3Cert among siblings.
It sits under the forcing-chain landmarks T5 (J uniqueness) and T8 (D=3). No recorded downstream consumers yet; it is infrastructure for metric positivity rather than a paper proposition in its own right.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.