domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass–energy pair is nonnegative. Anyone using the Module-7 cost functional on positive ratios cites this bound. The proof unfolds the definition and applies the standard AM-GM nonnegativity of J on the positive quotient.
Claim. For all real $m,e>0$, the domain cost of the pair $(m,e)$ satisfies $0 \le C_{\mathrm{dom}}(m,e)$. Equivalently, if the domain cost is the $J$-cost of the positive ratio $m/e$, then $J(m/e)\ge 0$.
background
Module 7 of the RS forcing chain records the exact count law $2^D-1=7$ independent observable categories at spatial dimension $D=3$. Costs in this layer are built from the Recognition $J$-functional
$$J(x)=\frac{x+x^{-1}}{2}-1=\frac{(x-1)^2}{2x}$$
(for $x>0$), which is the unique cost forced by the Recognition Composition Law (T5). The domain cost of a mass–energy pair is the $J$-cost of their positive ratio.
Upstream, Jcost_nonneg states that $J(x)\ge 0$ whenever $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM). That lemma is the only nontrivial input.
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J$ at $m/e$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma that $J$ is nonnegative on the positive reals.
why it matters
Nonnegativity of domain cost is the elementary positivity gate for any Module-7 argument that treats mass–energy imbalance as a cost. It sits under the structural count-law certificate of the module (exact $2^3-1=7$ categories at $D=3$) and inherits the T5 uniqueness of $J$. No downstream theorems currently depend on it in the graph, so it functions as a local hygiene lemma rather than a chain bottleneck. It does not itself force the octave or the dimension count; those are separate T7/T8 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.