domainCost_nonneg
plain-language theorem explainer
For positive real mass and energy parameters, the domain cost is nonnegative. Cosmology proofs that bound or compare domain costs on the phi-ladder cite this. The argument is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio.
Claim. For all real $m>0$ and $e>0$, the domain cost satisfies $0 \leq J(m/e)$, where $J(x)=(x+x^{-1})/2-1$ is the Recognition J-cost.
background
The module derives a structural match of the Planck Hubble value $H_0=67.4,\mathrm{km/s/Mpc}$ to an RS expression $H_0=\varphi^k/\tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}}=13.8,\mathrm{Gyr}$, framed as a zero-sorry structural theorem on the phi-ladder.
Domain cost is the local cost assigned to a positive mass–energy pair $(m,e)$ by evaluating the Recognition J-cost on the ratio $m/e$. The J-cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely in the T5 step of the unified forcing chain and obeying the Recognition Composition Law.
Upstream, Jcost_nonneg records that $J(x)\ge 0$ for every $x>0$, proved by rewriting $J$ as a square over a positive denominator (AM-GM / positivity).
proof idea
One-line wrapper. Unfold the definition of domain cost (so the goal becomes nonnegativity of $J(m/e)$). The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Discharge with the upstream lemma Jcost_nonneg on that positive ratio.
why it matters
Keeps every domain-cost comparison in the Hubble-precise certification on the nonnegative side of the J-cost, which is the same cost functional fixed by T5 and used throughout RS mass and coherence arguments. The module status is structural (0 sorry, 0 axiom) for the Planck $H_0$ match via $\varphi^k/\tau_{\mathrm{universe}}$; this lemma is the elementary positivity gate for that cost bookkeeping. No downstream consumers are recorded yet in the graph, so it presently serves the local certificate assembly (HubblePrecise2Cert and related siblings) rather than a named parent theorem outside the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.