domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters, the domain cost is nonnegative. Cosmology proofs that bound recombination thresholds via J-cost cite this. The argument is a one-line wrapper: unfold the domain cost to J of the mass-to-energy ratio, then apply J-cost nonnegativity.
Claim. If $m>0$ and $e>0$ are real, then the domain cost of the pair $(m,e)$ satisfies $0\le C_{\mathrm{dom}}(m,e)$. (Here $C_{\mathrm{dom}}(m,e)$ is the J-cost of the ratio $m/e$.)
background
The module derives the recombination redshift $z_{\mathrm{rec}}\approx 1100$ as a structural consequence of J-cost geometry on the $\varphi$-ladder: $\log 1100/\log\varphi\approx 14.7$, so $z_{\mathrm{rec}}$ sits between $\varphi^{14}$ and $\varphi^{15}$. Status is a structural theorem (no sorry, no axioms).
The J-cost is the Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law. Upstream, Jcost_nonneg records the elementary fact that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
Locally, domain cost is the specialization of $J$ to a positive mass-to-energy ratio $m/e$. Nonnegativity of that specialization is the first arithmetic guardrail before thresholds and certificates in the same file.
proof idea
One-line wrapper. Unfold the definition of domain cost, which is $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Feed that positivity into the upstream lemma Jcost_nonneg (AM-GM form of $J\ge 0$ on positives). No further algebra.
why it matters
Sits in the Cosmology track that ties recombination redshift to J-cost and the $\varphi$-ladder (module claim: $z_{\mathrm{rec}}=\varphi^k$ with $k\approx 14.7$). Nonnegativity is the baseline inequality any later comparison of domain cost against a canonical threshold must inherit; siblings include the domain-cost definition, equality-at-evaluation, the positive canonical threshold, and the recombination certificate bundle.
No downstream dependents are recorded yet, so the lemma is presently a local arithmetic lemma inside the recombination certificate construction rather than a cross-module export. It anchors the cost side of the structural story that places $z_{\mathrm{rec}}$ between $\varphi^{14}$ and $\varphi^{15}$, consistent with the eight-tick / $\varphi$-ladder landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.