summable_shift_rpow3
plain-language theorem explainer
The real p-series with exponent 3 remains summable after the index shift n ↦ n+1, i.e. ∑ 1/(n+1)³ converges. Cosmology proofs that feed Dirichlet data into Mellin identities at s = 3 cite it as the summability side-condition. The argument is a short reduction: classical p-series summability for p = 3, then Mathlib's nat-add shift equivalence and a termwise congruence.
Claim. The series $\sum_{n=0}^{\infty} 1/(n+1)^3$ of nonnegative reals is summable (equivalently, converges).
background
This module closes the number-density layer of thermal integrals at Mellin parameter $s = 3$. Photon number density is $n_\gamma = (g_\gamma/(2\pi^2)) T^3 \int_0^\infty t^2/(e^t-1),dt$, and the Bose integral equals $\Gamma(3)\zeta(3) = 2\zeta(3)$. The Fermi companion uses $\eta(3)$, giving the number-density fermion weight $\eta(3)/\zeta(3) = 3/4$.
The integral step rests on a Mellin/Dirichlet identity hasSum_mellin: geometric expansions of the Bose and Fermi kernels become Dirichlet series whose general term involves $1/(n+1)^s$ (or the alternating version). For the HasSum statements at $s = 3$ to fire, the shifted real $p$-series with exponent 3 must be summable.
Classical comparison: $\sum n^{-p}$ converges for real $p > 1$. Mathlib packages this as Real.summable_one_div_nat_rpow; the only remaining bookkeeping is the unit shift of the summation index.
proof idea
First obtain summability of $n \mapsto 1/n^3$ from Real.summable_one_div_nat_rpow with the numeric witness $3 > 1$ (norm_num). Apply summable_nat_add_iff at shift $1$ to move the sum to $m \mapsto 1/(m+1)^3$ in the shifted indexing. Finish with Summable.congr and a termwise identity (push_cast; ring_nf) equating the two presentations of the shifted summand.
why it matters
Without this lemma the Mellin side-conditions for number density fail. Downstream, hasSum_mellin_bose3 and hasSum_mellin_fermi3 invoke it (via hasSum_mellin) to identify
$\mathrm{mellin}(\mathrm{boseKernel},3) = \Gamma(3)\zeta(3)$ and $\mathrm{mellin}(\mathrm{fermiKernel},3) = \Gamma(3)\eta(3)$.
Those identities are the last analytic input to entropyPerPhoton_eq_ratio / entropyPerPhoton_from_integrals: they convert the thermodynamic ratio into pure zeta data and fix the fermionic number-density weight $3/4$ (companion of the $7/8$ entropy weight). In the broader RS cosmology stack this is the $s = 3$ twin of the already-closed energy-density layer at $s = 4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.