tail_summable
plain-language theorem explainer
The real series ∑ 1/(n+41)³ over n ∈ ℕ converges. Cosmology lemmas that trap the ζ(3) tail between telescoping bounds cite this to justify the infinite sums. Proof shifts Mathlib's p-series summability at exponent 3 by the index offset 41, then rewrites terms by casting and ring normalization.
Claim. The series $\sum_{n=0}^{\infty} 1/(n+41)^3$ of nonnegative reals is summable (converges).
background
This module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45\zeta(3))$ in the narrow 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_{n\ge 1} n^{-3}$.
The strategy splits $\zeta(3)$ after forty terms: the partial sum $S_{40}$ is pinned by exact rational arithmetic, and the tail $\sum_{n\ge 41} n^{-3}$ is rewritten as $\sum_{n=0}^{\infty} 1/(n+41)^3$. Before that tail can be compared termwise to telescoping majorants and minorants, the series must be known to converge so that the sum and HasSum infrastructure apply.
Mathlib already records that $\sum n^{-p}$ converges for real $p>1$; the local work is only the constant shift of the summation index and the identification of the shifted summand.
proof idea
Start from Mathlib's Real.summable_one_div_nat_pow at exponent $p=3$, discharged by norm_num since $3>1$. Apply summable_nat_add_iff 41 to shift the domain by forty-one, obtaining summability of $n\mapsto 1/(n+41)^3$ in the natural indexing. Finish by a pointwise congruence: push_cast and ring_nf identify the shifted Mathlib summand with the stated real expression. Pure existence of the sum; no numerical bound is produced here.
why it matters
Parent lemmas tail_ge and tail_le both invoke tail_summable.hasSum inside hasSum_le comparisons against the telescoping series $g_{\mathrm{Lo}}$ and $g_{\mathrm{Hi}}$. Those yield $1/3444\le\mathrm{tail}\le 1/3280$, which with the exact $S_{40}$ window closes
$$1.202042<\zeta(3)<1.202065$$
(true value $\approx 1.2020569$). Together with the $\pi^4$ window and the model arithmetic $g_{*s}=43/11$, this supplies the derived entropy-per-photon factor used by the baryogenesis dynamical prefactor. The lemma is pure analysis scaffolding inside a THEOREM-status cosmology derivation over Standard Model particle content; it does not itself touch the Recognition forcing chain (T0–T8) or the $\phi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.