hasSum_zeta3_shift
plain-language theorem explainer
The series ∑_{n≥0} 1/(n+1)³ equals Apéry's constant ζ(3) as an unconditional HasSum. Cosmology proofs that need the shifted Dirichlet series for Bose number-density Mellin transforms cite this. The argument is a one-line unwrap: unfold the definition of ζ(3) and apply the already-proved summability certificate.
Claim. The real series $\sum_{n=0}^{\infty} 1/(n+1)^3$ has sum equal to Apéry's constant $\zeta(3)$, where $\zeta(3)$ is defined as that same $t$-sum.
background
This module sits in the number-density layer of RS cosmology: it closes the Mellin integrals at $s=3$ that feed photon and fermion number densities, companion to the $s=4$ energy-density work in FermionWeightIntegral. The target identity is $\int_0^\infty t^2/(e^t-1),dt = \Gamma(3)\zeta(3)=2\zeta(3)$, which yields $n_\gamma=(2\zeta(3)/\pi^2)T^3$.
Apéry's constant is introduced upstream as the concrete real $t$-sum $\zeta(3):=\sum'_{n:\mathbb{N}} 1/(n+1)^3$, together with a summability lemma obtained from Mathlib's $p$-series criterion at $p=3$ after a unit shift. The present lemma simply packages that summable family as a HasSum with value exactly that constant. No closed form for $\zeta(3)$ is claimed or needed.
proof idea
One-line term proof. Unfold the definition of $\zeta(3)$ (the $t$-sum of $1/(n+1)^3$), then apply Summable.hasSum to the upstream lemma that this family is summable. No further algebraic rewriting is required.
why it matters
This is the base HasSum for the shifted cubic series. Downstream, hasSum_zeta3_unshifted moves the index by one (treating the $n=0$ term as $1/0=0$ in reals) so the unshifted Dirichlet series also sums to $\zeta(3)$. That form, and the shifted form directly, feed mellin_bose3_value: uniqueness of unconditional sums turns the geometric Bose kernel expansion into $\mathrm{mellin}(1/(e^t-1),3)=2\zeta(3)$.
Together with the Fermi companion $\eta(3)=(3/4)\zeta(3)$, these close the last analytic ingredient of the entropy-per-photon ratio rewrite. In the RS cosmology stack this is pure classical analysis scaffolding for thermodynamic integrals, not a forcing-chain (T0–T8) step; it supplies the number-density weight that dilutes fermionic species relative to photons before entropy bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.