domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Cosmology proofs that bound reionization endpoints via J-cost cite this inequality as a basic positivity lemma. The argument is a one-line wrapper: unfold the domain cost to J of the mass-to-energy ratio and apply the standard J-cost nonnegativity lemma.
Claim. Let $m,e\in\mathbb{R}$ with $m>0$ and $e>0$. Then the domain cost of the pair satisfies $0\le\mathrm{domainCost}(m,e)$. (Here domain cost is the J-cost of the ratio $m/e$.)
background
The module treats the end of cosmic reionization as a structural consequence of the Recognition Science J-cost. Observationally reionization finishes near $z\sim 5.5$–$6$; the RS sketch identifies the endpoint with a small power of the golden ratio $\varphi$ (e.g. $\varphi^3$ or $\varphi^4$), which sits in the same numerical band.
The cost functional is the unique J forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream, Jcost_nonneg records the elementary fact that $J(x)\ge 0$ on the positive reals, proved by rewriting $J$ as a square over a positive denominator (AM-GM).
In this file the domain cost of a mass–energy pair is defined so that it reduces exactly to $J(m/e)$. Nonnegativity of that quantity is therefore inherited from nonnegativity of $J$ once $m/e>0$ is known.
proof idea
One-line wrapper. Unfold the definition of domain cost; the body is $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos, so the standard lemma Jcost_nonneg applies directly and yields $0\le J(m/e)$.
why it matters
This is a local positivity fact inside the reionization-endpoint development (Plan v7 structural pass: zero sorry, zero axiom). Downstream certificates in the same module (canonical threshold positivity, the inhabited reionization-end certificate) rely on costs being well-behaved and nonnegative before they can be compared to $\varphi$-ladder thresholds.
In the broader RS chain, J-nonnegativity is the analytic shadow of T5 (J-uniqueness) and the Recognition Composition Law: the cost that measures departure from self-similar balance cannot go negative. The lemma therefore keeps the cosmology layer consistent with the forcing chain rather than introducing an ad-hoc energy functional.
No external parent theorem currently lists this declaration as a dependency; its role is internal hygiene for the reionization certificate stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.