domainCost_nonneg
plain-language theorem explainer
For positive mass and energy, the domain cost is nonnegative. Cosmology proofs that bound RS cost functionals inside inflation-parameter certificates cite this fact. The proof is a one-line unfold of domain cost into ordinary J-cost on the mass-to-energy ratio, then the standard AM-GM nonnegativity lemma.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative. Equivalently, if $J(x)=\frac{x+x^{-1}}{2}-1$ denotes the Recognition Science cost, then $0\le J(m/e)$.
background
The module records structural RS inflation parameters: scalar index $n_s=1-2/45\approx0.9556$ (within $2.1\sigma$ of the reported $0.9649$) and tensor-to-scalar ratio $r=2/(45\varphi^2)\approx0.0169<0.036$. Status is a fully proved structural theorem (zero sorry, zero axiom).
Domain cost is the local packaging of the J-cost on a positive mass-to-energy ratio. The underlying cost is the unique functional forced by the Recognition Composition Law and the T5 step of the forcing chain: $J(x)=\cosh(\log x)-1=(x+x^{-1})/2-1$ for $x>0$. Upstream lemmas establish $J(x)\ge0$ for every positive $x$, either by rewriting $J$ as the square $(x-1)^2/(2x)$ or by the AM-GM bound $x+x^{-1}\ge2$.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The two positivity hypotheses give $m/e>0$ by div_pos. Discharge the goal by the upstream lemma Jcost_nonneg (AM-GM / squared form of $J$).
why it matters
Local hygiene lemma inside the Inflation Parameters5 certificate stack. It guarantees that every domain-cost evaluation used when comparing RS predictions for $n_s$ and $r$ against observational bands sits above zero, so cost comparisons cannot flip sign by accident. No external used_by edges are recorded yet; the immediate consumers are the sibling certificate constructors (InflationParam5Cert, cert, cert_inhabited) in the same module. The result inherits its force from T5 J-uniqueness rather than from any new cosmological hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.