zeta3_summable
plain-language theorem explainer
The real series ∑ 1/(n+1)³ over n ∈ ℕ converges. Cosmology and analysis proofs cite it to treat ζ(3) as a well-defined real and to split or identify that series. The argument is a short Mathlib reduction: p-series summability at p = 3, then a unit index shift and termwise algebraic congruence.
Claim. The series $\sum_{n=0}^{\infty} 1/(n+1)^3$ is summable as a series of real numbers (equivalently, it converges in $\mathbb{R}$).
background
This module derives the entropy-per-photon ratio $s/n_\gamma = \pi^4 g_{*s}/(45,\zeta(3))$ in a narrow window around 7.04, for the baryogenesis dynamical lane. One ingredient is a rigorous real value for Apéry's constant via the shifted p-series
$$\zeta(3) := \sum_{n=0}^{\infty} 1/(n+1)^3.$$
Summability is the prerequisite for that definition as a tsum and for any later split into a finite head plus a tail. Mathlib already knows that $\sum 1/n^p$ converges for real $p>1$; here $p=3$. The shift from $\sum_{n\ge 1} 1/n^3$ to $\sum_{n\ge 0} 1/(n+1)^3$ is the standard nat_add reindexing, so the two series converge or diverge together.
proof idea
Apply Real.summable_one_div_nat_pow at $p=3$; the hypothesis $3>1$ is discharged by norm_num, yielding summability of $n\mapsto 1/n^3$ on $\mathbb{N}$. Transport across the unit shift with summable_nat_add_iff 1. Finish by Summable.congr: after push_cast, ring_nf identifies $1/((n:\mathbb{R})+1)^3$ with the shifted term. No ε-δ work is local to this file.
why it matters
Without summability, zeta3 is not a real number and the entropy-per-photon THEOREM cannot start. Downstream, zeta3_split uses zeta3_summable.sum_add_tsum_nat_add 40 to cut the series at 40 terms (exact head by norm_num, telescoping tail bounds). NumberDensityIntegral.hasSum_zeta3_shift packages the same fact as HasSum, identifying the defining sum with zeta3 for number-density integrals. Together these feed the ζ(3) window $1.202042 < \zeta(3) < 1.202065$ that, with the $\pi^4$ window and $g_{*s}=43/11$, replaces the bare constant 7.04 in the baryogenesis prefactor. Landmark link is cosmological bookkeeping (entropy degrees of freedom), not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.