domainCost_nonneg
plain-language theorem explainer
The domain cost of a positive mass-energy pair is nonnegative. Anyone treating Recognition cost on configuration ratios cites this positivity fact before thresholds or certificates. The proof is a one-line wrapper: unfold the domain cost to J on the mass-to-energy ratio, then apply J-nonnegativity via AM-GM.
Claim. For all real $m,e>0$, the domain cost of the pair is nonnegative: $0\leq J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition cost on the positive ratio $m/e$.
background
Recognition Science takes the unique cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$), forced by the Recognition Composition Law at T5. On $x>0$, $J(x)\geq 0$ by AM-GM, with equality only at $x=1$. Upstream lemmas record this as $J$-cost nonnegativity, often by rewriting $J(x)=(x-1)^2/(2x)$.
This module (Foundation RS Module 6) is a structural slice of the forcing chain: configuration dimension $D=3$ is forced by the eight-tick period $2^3$, with no free parameters. Domain cost packages $J$ on a mass-energy ratio $m/e$, the natural dimensionless argument for cost comparisons on the $\phi$-ladder.
The local setting is a zero-sorry structural certificate module; positivity of domain cost is the elementary defect check before canonical thresholds and the module cert bundle.
proof idea
One-line wrapper. Unfold domain cost (definitionally $J$ of the ratio $m/e$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge the goal by the upstream lemma that $J(x)\geq 0$ for every positive real $x$ (AM-GM / square form of $J$).
why it matters
Sits in Foundation Module 6 of the RS forcing chain, whose module doc records $D=3$ forced from the eight-tick octave $2^3$ (T7, T8) with status structural theorem (0 sorry, 0 axiom). Nonnegativity makes domain cost a genuine defect measure, so sibling threshold and certificate objects (canonical threshold positivity, the Module 6 cert) can treat it as a cost rather than a signed score.
No downstream uses are recorded in the graph yet; the lemma is local infrastructure for the module cert bundle. It inherits T5 $J$-uniqueness: once $J$ is the unique cost functional, every ratio-based domain cost is automatically nonnegative on positive data. Does not itself force dimension or the octave; those live in the surrounding certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.