hasSum_gHi
plain-language theorem explainer
The successive differences of the upper telescoping comparator gHi form a series that sums exactly to gHi(0). Cosmologists bounding the ζ(3) tail cite this to convert the pointwise inequality 1/(n+41)³ ≤ gHi(n)−gHi(n+1) into a numerical upper bound. The proof is a telescoping partial-sum identity plus the already-proved limit gHi→0.
Claim. Let $g_{\mathrm{hi}}(n)=1/(2(n+40)(n+41))$. The series of nonnegative terms $g_{\mathrm{hi}}(n)-g_{\mathrm{hi}}(n+1)$ is summable and $\sum_{n=0}^{\infty}\bigl(g_{\mathrm{hi}}(n)-g_{\mathrm{hi}}(n+1)\bigr)=g_{\mathrm{hi}}(0)$.
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$, obtained by evaluating the first 40 terms exactly and trapping the tail $\sum_{n\ge 41}1/n^3$ between two telescoping rational series.
The upper comparator is $g_{\mathrm{hi}}(n)=1/(2(n+40)(n+41))$. Its consecutive differences equal $1/((n+40)(n+41)(n+42))$, which dominates $1/(n+41)^3$. Upstream, $g_{\mathrm{hi}}$ is antitone in the sense that each difference is nonnegative, and $g_{\mathrm{hi}}(n)\to 0$ as $n\to\infty$ by a squeeze against $1/(n+\mathrm{const})$.
proof idea
Apply the Mathlib criterion that a nonnegative series has sum $s$ iff its partial sums tend to $s$, using nonnegativity from gHi_antitone. The partial sum over Finset.range n collapses by the standard telescoping identity Finset.sum_range_sub' to $g_{\mathrm{hi}}(0)-g_{\mathrm{hi}}(n)$. Subtract the constant sequence from the already-proved limit gHi_tendsto to obtain the required convergence to $g_{\mathrm{hi}}(0)$.
why it matters
Feeds directly into tail_le, which concludes that the $\zeta(3)$ tail is at most $g_{\mathrm{hi}}(0)=1/3280$. That bound, paired with the matching lower telescoping comparator and the exact $S_{40}$ rational window, yields $1.202042<\zeta(3)<1.202065$. Together with the $\pi^4$ window and the arithmetic identity $g_{*s}=43/11$ from Standard Model particle content (photon, $e^\pm$, three neutrino generations, with the $7/8$ fermion weight now theorem-level), this closes the analytic half of the entropy-per-photon derivation used by the baryogenesis dynamical prefactor. No Recognition forcing-chain step (T0–T8) is invoked here; the lemma is pure real analysis supporting a cosmology constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.