domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Cosmologists checking the SGWB phi-ladder estimates in this module would cite it as a basic positivity guard. The proof is a one-line wrapper: unfold the cost and apply the standard J-cost nonnegativity lemma at the positive ratio.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0 \le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
The module treats the stochastic gravitational wave background (SGWB) as a structural consequence of the phi-ladder: a claimed RS relation $\Omega_{\mathrm{GW}}=J(\phi)^2\Omega_{\mathrm{matter}}$ is contrasted with the much smaller nHz observational band. Status is structural (no sorry, no axioms).
The Recognition cost $J$ is the unique nonnegative functional forced by the composition law (T5): $J(x)=(x+x^{-1})/2-1$ for $x>0$, equivalently $(x-1)^2/(2x)$. Upstream lemmas record $J(x)\ge 0$ for every positive $x$, proved by AM-GM or by rewriting as a square over a positive denominator.
Here the domain cost of a mass-energy pair is that same $J$ evaluated at the positive ratio $m/e$. Positivity of the ratio is the only extra hypothesis needed to invoke the cost lemma.
proof idea
One-line wrapper. Unfold domainCost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the upstream lemma Jcost_nonneg (AM-GM / square form of $J$).
why it matters
Keeps every domain-cost appearance in the SGWB structural development inside the nonnegative cone required by Recognition cost theory. The module frames $\Omega_{\mathrm{GW}}$ estimates against $J(\phi)$ and matter density; without this guard, later comparisons of ladder amplitudes to the nHz band would sit on an unsigned quantity.
No downstream consumers are recorded yet (used_by is empty), so the lemma is presently a local hygiene fact for the SGWB3 certificate siblings (canonicalThreshold_pos, SGWB3Cert, cert). It sits under the T5 J-uniqueness landmark: once $J$ is forced, every specialized cost inherits nonnegativity for free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.