domainCost_nonneg
plain-language theorem explainer
Domain cost of a positive mass–energy pair is nonnegative. Cosmology proofs that certify the RS reionization window (phi^4–phi^5 bracketing z_reion) cite this as the basic positivity fact. The proof is a one-line unfold of domainCost followed by J-cost nonnegativity on the ratio m/e.
Claim. For all real $m,e>0$, the domain cost satisfies $0\le J(m/e)$, where $J$ is the Recognition cost $J(x)=(x+x^{-1})/2-1$.
background
The module treats reionization redshift in Recognition Science units. Observed $z_{\mathrm{reion}}\sim 7$–$10$ sits between the golden-ratio powers $\varphi^4\approx 6.85$ and $\varphi^5\approx 11.09$, so the RS ladder brackets the epoch without free parameters.
Domain cost is the local cost assigned to a positive mass–energy pair $(m,e)$. From the proof shape it is exactly the J-cost of the ratio: $\mathrm{domainCost}(m,e)=J(m/e)$. The J-cost itself is the unique nonnegative generator forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, with $J(x)\ge 0$ for all $x>0$ by AM-GM.
Upstream, Jcost_nonneg records that nonnegativity (proved via the squared form $(x-1)^2/(2x)$ or by $x+x^{-1}\ge 2$).
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes $0\le J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the standard lemma Jcost_nonneg to that positive ratio.
why it matters
Positivity of domain cost is the elementary inequality needed before any threshold comparison in the reionization certificate stack (siblings: canonicalThreshold_pos, ReionizationCert, cert_inhabited). The module is marked STRUCTURAL THEOREM (zero sorry, zero axiom) and sits in the cosmology layer that links the phi-ladder to observed $z_{\mathrm{reion}}$.
In the broader forcing chain, J-nonnegativity is the content of T5 uniqueness; here it is simply re-exported at the mass–energy ratio that the reionization domain uses. No downstream dependents are recorded yet, so the lemma is presently a local hygiene fact for the certificate constructors in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.