hasSum_zeta_shift
plain-language theorem explainer
The index-shifted fourth Basel sum ∑_{n≥0} 1/(n+1)^4 converges unconditionally to π⁴/90. Cosmology proofs that evaluate Bose–Einstein Mellin transforms at s=4 cite this so the Dirichlet side matches the geometric expansion 1/(e^t−1)=∑ e^{−(n+1)t}. The argument reindexes Mathlib's standard ζ(4) HasSum by shifting the natural-number origin by one via the add-iff lemma.
Claim. The series $\sum_{n=0}^{\infty} 1/(n+1)^4$ converges unconditionally (as a real `HasSum`) to $\pi^4/90$. Equivalently, the index-shifted representation of $\zeta(4)$ equals the classical Basel value at order four.
background
This module sits at the thermodynamic layer of the fermion-weight chain. Cosmology.FermionWeight already supplies the series identity $\eta(4)=(7/8)\zeta(4)$. What remains is to pass from those Dirichlet series to the energy integrals
$$\int_0^\infty t^3/(e^t\pm 1),dt,$$
which are the Mellin transforms at $s=4$ of the geometric kernels $1/(e^t-1)=\sum_{n\ge 0}e^{-(n+1)t}$ and $1/(e^t+1)=\sum_{n\ge 0}(-1)^n e^{-(n+1)t}$. Mathlib's Mellin-of-power-series lemma converts each kernel into $\Gamma(4)$ times a shifted zeta or eta sum; $\Gamma(4)=6$ then yields the closed forms $\pi^4/15$ (Bose) and $7\pi^4/120$ (Fermi).
The present lemma is the Bose half of that Dirichlet evaluation: the sum must start at $n=0$ with denominator $(n+1)^4$ to line up with the geometric indexing. The classical Mathlib fact $\sum_{m\ge 1}1/m^4=\pi^4/90$ is therefore only one reindexing away.
proof idea
Begin from Mathlib's unconditional sum for $1/m^4$, written so the $m=0$ slot is absorbed into a finite Finset.range 1 correction and the total equals $\pi^4/90$ plus that correction. Apply the natural-number shift equivalence (hasSum_nat_add_iff at offset 1) in the reverse direction: dropping the first term and reindexing produces a HasSum for $n\mapsto 1/(n+1)^4$. A final congr_fun with push_cast and ring identifies the summand with the stated formula, and the finite correction cancels, leaving value $\pi^4/90$.
why it matters
Parent uses are immediate. mellin_bose_value multiplies this sum by $\Gamma(4)=6$ and invokes uniqueness of HasSum to conclude
$$\mathrm{mellin}\bigl(1/(e^t-1)\bigr)(4)=\pi^4/15.$$
RadiationEntropyRelation.mellin_boseLog_value does the same with factor 2 for the logarithmic Bose kernel at $s=3$, obtaining $\pi^4/45$. Together with the parallel eta-shift lemma, these close the integral identities
$$\int t^3/(e^t-1)=\pi^4/15,\qquad \int t^3/(e^t+1)=7\pi^4/120,$$
so the ratio $7/8$ is theorem-level. Per the module doc, the entire mathematical content of EntropyPerPhoton.fermionWeight=7/8 is then proved; only the $g^*$ species census remains model-side bookkeeping. No T0–T8 forcing step is touched; this is pure analytic scaffolding for the radiation-entropy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.