domainCost_nonneg
plain-language theorem explainer
For positive mass and energy scales, the domain cost of their ratio is nonnegative. Anyone comparing domain costs to canonical thresholds in the φ-ladder string-compactification package would cite this. The proof is a one-line unfold of the domain-cost definition, then the standard nonnegativity of J-cost on positive reals.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ (the $J$-cost of the ratio $m/e$) is nonnegative: $0 \le J(m/e)$.
background
The module treats string compactification radii on the φ-ladder: extra dimensions sit at $R_{\mathrm{comp}}=\ell_{\mathrm{Pl}},\varphi^{-k}$, with $k=0$ near the Planck scale and $k\approx 106$ near the electroweak scale. Status is structural (zero sorry, zero axiom).
The Recognition cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, forced unique by the Recognition Composition Law (T5). Upstream lemmas prove $J(x)\ge 0$ for every $x>0$, either by rewriting $J(x)=(x-1)^2/(2x)$ or by AM-GM on $x+x^{-1}\ge 2$.
In this file the domain cost of mass $m$ and energy $e$ is exactly that $J$ evaluated at the positive ratio $m/e$. Nonnegativity is therefore inherited from the cost calculus rather than from any string-specific geometry.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). Discharge the positivity side-condition by div_pos on the two hypotheses $m>0$ and $e>0$, then apply the upstream lemma Jcost_nonneg.
why it matters
Local infrastructure inside the φ-ladder string-length package. Sibling declarations (canonical threshold positivity, string-length certificates, inhabited certs) need a nonnegative domain cost before they can compare costs to thresholds or assert certificate inhabitation. The result sits under the T5 J-uniqueness landmark: once $J$ is forced and known nonnegative, every derived cost (here the mass-to-energy domain cost) inherits the same sign. No external used-by edges are recorded yet; the lemma closes a positivity obligation inside this structural module rather than feeding a later global theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.