hasSum_zeta3_unshifted
plain-language theorem explainer
The series ∑_{n≥0} 1/n³ equals Apéry's constant ζ(3), with the n=0 term read as zero. Cosmology arguments that split ζ(3) into even and odd parts cite this to work over all of ℕ rather than the shifted defining sum. The proof transports the defining HasSum across a unit index shift via Mathlib's hasSum_nat_add_iff.
Claim. The series $\sum_{n=0}^{\infty} n^{-3}$ HasSums to Apéry's constant $\zeta(3)$, where the $n=0$ summand is interpreted as $0$.
background
This module closes the number-density Mellin layer at $s=3$: Bose $\int_0^\infty t^2/(e^t-1),dt=2\zeta(3)$ and Fermi $\int_0^\infty t^2/(e^t+1),dt=(3/2)\zeta(3)$, so the fermion number-density weight is $\eta(3)/\zeta(3)=3/4$. That weight is the last analytic input to the photon number density $n_\gamma=(2\zeta(3)/\pi^2)T^3$ and to entropyPerPhoton_eq_ratio.
Apéry's constant is defined in EntropyPerPhoton as the tsum $\zeta(3):=\sum'_n 1/(n+1)^3$. The sibling lemma records that this shifted series HasSums to $\zeta(3)$. The unshifted series $\sum 1/n^3$ over all of $\mathbb{N}$ (with $1/0^3=0$) is the form needed for the even/odd split that produces $\eta(3)$.
proof idea
Begin from the sibling HasSum of $n\mapsto 1/(n+1)^3$ to $\zeta(3)$. A pointwise congruence (push_cast; ring) rewrites the summand in natural-number form. Mathlib's hasSum_nat_add_iff at shift $1$ converts that shifted HasSum into a HasSum of $n\mapsto 1/n^3$ over all of $\mathbb{N}$; the dropped initial segment is the single $n=0$ term, which vanishes. A final simpa closes the goal. Term-mode, three steps, no new analysis.
why it matters
Entry point for the series-layer even/odd decomposition of $\zeta(3)$. Downstream, the even-part lemma obtains $\sum_k 1/(2k)^3=\zeta(3)/8$ by dividing this unshifted sum by 8; summability and HasSum of the odd part then recover $(7/8)\zeta(3)$ by uniqueness of unconditional sums. Those identities give $\eta(3)=(3/4)\zeta(3)$, the number-density fermion weight (companion of the $7/8$ entropy weight). That ratio feeds the integral-layer Mellin evaluation and the rewrite of entropy-per-photon as a pure ratio of thermodynamic integrals. Without the unshifted form, the even-index extraction does not line up with the geometric series kernels at $s=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.