hasSum_eta3_shift
plain-language theorem explainer
The index-shifted alternating cubic series equals three-quarters of Apéry's constant: ∑_{n≥0} (−1)^n/(n+1)³ = η(3) = (3/4)ζ(3). Cosmology proofs that evaluate fermionic number-density Mellin transforms at s=3 cite this form. The argument reindexes the unshifted η(3) HasSum by one and matches terms by elementary algebra.
Claim. The series $\sum_{n=0}^{\infty} (-1)^n/(n+1)^3$ converges unconditionally to $(3/4)\,\zeta(3)$, where $\zeta(3)=\sum_{n=0}^{\infty} 1/(n+1)^3$ is Apéry's constant.
background
This module closes the number-density layer of thermal integrals at Mellin parameter $s=3$. Photon number density is $n_\gamma=(2\zeta(3)/\pi^2)T^3$; the fermionic companion uses the Dirichlet eta value $\eta(3)=(3/4)\zeta(3)$, so the number-density fermion weight is $\eta(3)/\zeta(3)=3/4$ (the analogue of the $7/8$ entropy weight).
Apéry's constant is defined here as the real tsum $\zeta(3)=\sum'_{n} 1/(n+1)^3$. The unshifted alternating series $\sum (-1)^{n+1}/n^3$ is already known to HasSum to $(3/4)\zeta(3)$ by splitting $\zeta(3)$ into even and odd parts (even contribution $\zeta(3)/8$). The present lemma is the same sum written with index starting at zero and denominator $(n+1)^3$, which is the form fed to the Mellin/HasSum bridge for the Fermi kernel.
proof idea
Start from hasSum_eta_three, which supplies HasSum of $m\mapsto (-1)^{m+1}/m^3$ to $(3/4)\zeta(3)$ (with a dummy finite-range correction that vanishes after the shift). Apply Mathlib's hasSum_nat_add_iff at offset $1$ to reindex the domain from $\mathbb{N}$ starting at $1$ down to starting at $0$. Congruence of summands is a one-line push_cast plus pow_succ and ring: $(-1)^{n+1}/(n+1)^3$ matches $(-1)^n/(n+1)^3$ up to the sign bookkeeping already present in the base series.
why it matters
Downstream, mellin_fermi3_value multiplies this HasSum by $2$ and identifies the Mellin transform of the Fermi kernel $1/(e^t+1)$ at $s=3$ with $\Gamma(3)\eta(3)=(3/2)\zeta(3)$. That identity is the last analytic input to the number-density half of entropyPerPhoton_eq_ratio: Bose gives $\int t^2/(e^t-1)=2\zeta(3)$, Fermi gives $\int t^2/(e^t+1)=(3/2)\zeta(3)$, hence the $3/4$ fermion number weight that dilutes $n_\nu/n_\gamma$ before entropy dilution.
In the Recognition cosmology stack this sits beside the $s=4$ energy-density integrals already closed in FermionWeightIntegral. It does not touch the forcing chain (T5–T8) or RCL directly; it is pure classical analysis packaging $\eta(3)$ for the thermodynamic ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.