domainCost_nonneg
plain-language theorem explainer
The domain cost of any positive mass–energy pair is nonnegative. Cost and gravity modules cite this when they need a sign bound on the domain functional before thresholds or certificates. The argument is a one-line wrapper: unfold the domain cost to the J-cost of the mass-to-energy ratio, then apply J-nonnegativity via AM-GM.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0 \le C_{\mathrm{dom}}(m,e)$, where $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.
background
Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the forcing chain. For $x>0$, $J(x)\ge 0$ by AM-GM; equality holds only at $x=1$. The Cost module records this as Jcost_nonneg.
In this certificate module the domain cost of a mass–energy pair is defined by evaluating that same J-cost on the ratio $m/e$. The module is the RS 2026 state-of-the-art structural certificate: forcing chain T0–T8 complete, zero sorries, constants and cosmological parameters derived.
Upstream, three parallel nonnegativity lemmas (Cost, CoherenceCollapse, EnergyProcessingBridge) all state $J(x)\ge 0$ for $x>0$, proved either by rewriting $J$ as a square over a positive denominator or by the elementary bound $x+x^{-1}\ge 2$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. Positivity of the ratio follows from div_pos on the two strict positivity hypotheses. Discharge the goal by the upstream lemma Jcost_nonneg (AM-GM / square form of $J$).
why it matters
Local sign lemma inside the RS 2026 structural certificate. It anchors every later use of domain cost as a genuine cost (nonnegative, vanishing only on balance $m=e$) before canonical thresholds and the inhabited certificate RS2026State3Cert in the same module. Framework-wise it is the domain-level shadow of T5 J-uniqueness and the Recognition Composition Law: the same $J$ that is forced unique and nonnegative on ratios remains nonnegative when the ratio is interpreted as mass over energy. No downstream edges are recorded yet; the lemma is infrastructure for the certificate rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.