hasSum_gLo
plain-language theorem explainer
The successive differences of the lower telescoping comparator for the ζ(3) tail form a series summing to the comparator at zero. Anyone trapping the Apéry-constant tail from below by 1/(2(n+41)(n+42)) cites this. The proof rewrites HasSum as a limit of partial sums, telescopes by the finite-difference identity, and subtracts the known limit of the comparator to zero.
Claim. Let $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$. Then $\sum_{n=0}^{\infty}\bigl(g_{\mathrm{lo}}(n)-g_{\mathrm{lo}}(n+1)\bigr)$ converges in $\mathbb{R}$ and equals $g_{\mathrm{lo}}(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)$ from three ingredients: a $\zeta(3)$ window, a $\pi^4$ window, and $g_{*s}=43/11$ from Standard Model particle content. The $\zeta(3)$ bound splits the series at 40 terms; the tail $\sum_{n\ge 41}1/n^3$ is trapped by two telescoping comparators.
The lower comparator is $g_{\mathrm{lo}}(n)=1/(2(n+41)(n+42))$. Its consecutive differences equal $1/((n+41)(n+42)(n+43))\le 1/(n+41)^3$, so the summed differences under-estimate the tail. Upstream facts used here: the differences are nonnegative ($g_{\mathrm{lo}}$ is antitone in the discrete sense), and $g_{\mathrm{lo}}(n)\to 0$ as $n\to\infty$ by a squeeze against $1/(n+c)$.
proof idea
Term-mode argument in three steps. First rewrite HasSum via the nonnegative criterion: because consecutive differences are nonnegative (from the antitone lemma), HasSum is equivalent to the partial-sum sequence tending to the claimed total. Second, the finite telescoping identity Finset.sum_range_sub' gives $\sum_{i<n}(g_{\mathrm{lo}}(i)-g_{\mathrm{lo}}(i+1))=g_{\mathrm{lo}}(0)-g_{\mathrm{lo}}(n)$. Third, substitute and pass to the limit: constant sequence $g_{\mathrm{lo}}(0)$ minus $g_{\mathrm{lo}}\to 0$ yields $g_{\mathrm{lo}}(0)$.
why it matters
Feeds the lower tail bound tail_ge, which asserts $\sum_{n\ge 0}1/(n+41)^3\ge g_{\mathrm{lo}}(0)=1/3444$. That inequality, paired with the matching upper telescope, closes the $\zeta(3)$ window $1.202042<\zeta(3)<1.202065$ used in the entropy-per-photon derivation. The module replaces the bare constant $7.04$ in the baryogenesis dynamical prefactor by a fully derived interval. Within Recognition Science this is analysis-plus-arithmetic scaffolding for the cosmology lane, not a forcing-chain (T0–T8) step; it sits downstream of the fermion-weight theorems that justify the $7/8$ factor in $g_{*s}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.