gLo_nonneg
plain-language theorem explainer
For every natural number n, the lower telescoping comparator gLo(n) = 1/(2(n+41)(n+42)) is nonnegative. Cosmology proofs that trap the ζ(3) tail via squeeze arguments cite this. The proof unfolds the definition and applies Mathlib positivity.
Claim. For every natural number $n$, the lower telescoping comparator $g_{\mathrm{lo}}(n) := \frac{1}{2(n+41)(n+42)}$ satisfies $0 \le g_{\mathrm{lo}}(n)$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the window $(7.0393, 7.0396)$, replacing a bare $7.04$ constant in the baryogenesis lane. One ingredient is a rigorous window on $\zeta(3)=\sum 1/(n+1)^3$: a partial sum through 40 terms plus a trapped tail.
The lower comparator $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$ comes from the telescoping identity $1/(2(n+41)(n+42))-1/(2(n+42)(n+43))=1/((n+41)(n+42)(n+43))\le 1/(n+41)^3$. It is the pointwise lower envelope used to bound the $\zeta(3)$ tail from below by a convergent series that tends to zero at infinity.
Nonnegativity of this comparator is the first hypothesis of the squeeze lemma that shows $g_{\mathrm{lo}}\to 0$ along $\mathbb{N}$.
proof idea
One-line tactic proof: unfold the definition of $g_{\mathrm{lo}}$, then invoke Mathlib's positivity tactic. The denominator $2(n+41)(n+42)$ is a product of positive reals for every natural $n$, so the reciprocal is nonnegative.
why it matters
Feeds gLo_tendsto, which proves $g_{\mathrm{lo}}\to 0$ at infinity by squeeze_zero against a standard $1/(n+c)$ null sequence. That limit, together with the matching upper comparator, closes the tail estimate $1/3444\le\mathrm{tail}\le 1/3280$ and yields the $\zeta(3)$ window $1.202042<\zeta(3)<1.202065$.
The window is one of three THEOREM ingredients (with $\pi^4$ and $g_{*s}=43/11$) that pin $s/n_\gamma\in(7.0393,7.0396)$ for the baryogenesis dynamical prefactor. It is pure analysis over Standard Model particle content, not a Recognition forcing step (T0–T8), but it hardens a numerical constant the cosmology lane previously treated as bare input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.