gLo_tendsto
plain-language theorem explainer
The lower telescoping comparator for the ζ(3) tail, g_lo(n) = 1/(2(n+41)(n+42)), tends to 0 as n → ∞. Anyone assembling the HasSum of the telescoping differences for the ζ(3) tail bound cites this. The proof is a squeeze: nonnegativity plus an elementary comparison to 1/(n+1) via nlinarith.
Claim. Let $g_{\mathrm{lo}}(n) = 1/(2(n+41)(n+42))$ for $n \in \mathbb{N}$. Then $g_{\mathrm{lo}}(n) \to 0$ as $n \to \infty$ in $\mathbb{R}$.
background
The module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the band $(7.0393, 7.0396)$ from three ingredients: a $\zeta(3)$ window, a $\pi^4$ window, and $g_{*s} = 43/11$ from Standard Model particle content. The $\zeta(3)$ window splits the series at 40 terms and traps the tail by two telescoping comparators.
The lower comparator is the sequence $g_{\mathrm{lo}}(n) = 1/(2(n+41)(n+42))$. Its consecutive differences telescope and dominate $1/(n+41)^3$ from below, so the sum of those differences supplies the lower tail bound $1/3444 \le \sum_{n\ge 41} 1/n^3$. Nonnegativity of $g_{\mathrm{lo}}$ is already recorded as a one-line positivity lemma.
Convergence of $g_{\mathrm{lo}}$ to zero is the remaining analytic fact needed before the partial-sum identity can be turned into a HasSum statement for the telescoping series.
proof idea
Apply Mathlib's squeeze_zero with three ingredients: the already-proved nonnegativity of $g_{\mathrm{lo}}$, the standard limit $1/(n+1)\to 0$ at infinity, and a pointwise upper bound $g_{\mathrm{lo}}(n)\le 1/(n+1)$.
The bound is obtained by unfolding the definition, clearing positive denominators with div_le_div_iff₀, and finishing by nlinarith using Nat.cast_nonneg. No series machinery is needed; the argument is pure real arithmetic plus squeeze.
why it matters
Downstream, hasSum_gLo rewrites the HasSum of consecutive differences $g_{\mathrm{lo}}(n)-g_{\mathrm{lo}}(n+1)$ as the constant-minus-tail limit $g_{\mathrm{lo}}(0)-g_{\mathrm{lo}}(n)$, then subtracts this tendsto fact from a constant filter to conclude the sum equals $g_{\mathrm{lo}}(0)$. That HasSum is the lower half of the telescoping trap on the $\zeta(3)$ tail.
Closing the $\zeta(3)$ window is one of the three THEOREM ingredients that replace the bare constant $7.04$ in the baryogenesis dynamical prefactor by a derived interval $(7.0393, 7.0396)$. The lemma is pure analysis; it does not touch the Recognition forcing chain (T0–T8) or the RCL, but it is load-bearing for the cosmology lane that feeds those constants into the dynamical story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.