domainCost_nonneg
plain-language theorem explainer
For positive mass and energy parameters the domain cost is nonnegative. Cosmology certificates that bound RS predictions against the lithium-7 Spite plateau use this to keep cost terms on the admissible side of inequalities. The argument is a one-line wrapper: unfold the cost and apply J-cost nonnegativity to the positive ratio m/e.
Claim. For all real $m>0$ and $e>0$, the domain cost of the pair $(m,e)$ is nonnegative: $0\le C_{\mathrm{dom}}(m,e)$.
background
Module RS_Cosmo_Module_012 packages structural facts for the lithium-7 Spite plateau comparison: RS band $(4.69,4.86)\times 10^{-10}$ against the observed window $(4.0,5.2)\times 10^{-10}$, marked RS_PASS with no sorry and no axioms.
The domain cost is the local cost functional on a positive mass-energy pair. From the proof shape it is the J-cost of the ratio $m/e$. The J-cost is the standard Recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $(x-1)^2/(2x)$), forced unique by 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 to a square over a positive denominator (AM-GM). That lemma is the only nontrivial input here.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. Positivity of the ratio follows from div_pos on the two hypotheses $m>0$ and $e>0$. Discharge with the upstream lemma that $J(x)\ge 0$ for $x>0$.
why it matters
Nonnegativity of domain cost is a structural hygiene fact inside the cosmology certificate pack for the Li-7 Spite plateau (Module 012). Downstream use list is empty in the graph, so this lemma is presently a leaf: it stands ready for any inequality that needs $C_{\mathrm{dom}}\ge 0$ when comparing RS bands to observed abundance windows.
In the broader framework it inherits the T5 uniqueness of $J$ and the global convention that recognition costs are nonnegative on positive scales. It does not itself touch the eight-tick octave, $D=3$, or the alpha band; those enter only if a parent certificate later folds domain cost into a full cosmological forcing argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.