summable_shift_rpow
plain-language theorem explainer
The shifted real p-series ∑ 1/(n+1)^4 over naturals is summable. Cosmology proofs cite it as the absolute-convergence side condition for Mellin/Dirichlet identities of the Bose and Fermi kernels at s=4, and again for the logarithmic kernels in the radiation-entropy chain. The argument is a short reduction: Mathlib's unshifted p-series test, the nat-add shift equivalence, and a termwise congruence.
Claim. The real series $\sum_{n=0}^{\infty} \frac{1}{(n+1)^{4}}$ is summable (converges absolutely in $\mathbb{R}$).
background
This module sits at the integral (thermodynamic) layer of the fermion-weight story. The sibling module already has the Dirichlet identity $\eta(4)=(7/8)\zeta(4)$. Here the goal is the matching energy-integral statement
$\int_0^\infty t^3/(e^t+1),dt = (7/8)\int_0^\infty t^3/(e^t-1),dt$,
with both sides closed via $\Gamma(4)\zeta(4)$ and $\Gamma(4)\eta(4)$.
Both integrands arise as Mellin transforms at $s=4$ of geometric series in $e^{-t}$. Mathlib's Mellin-of-power-series lemma needs a summable Dirichlet side $\sum |a_n|/(n+1)^{\mathrm{Re},s}$. At $s=4$ with unit (or alternating) coefficients that side is exactly the shifted real $p$-series with exponent 4, which this lemma records.
Notation: the shift $n\mapsto n+1$ matches the geometric expansions $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}$ for $t>0$.
proof idea
Start from Mathlib's real $p$-series test: $\sum 1/n^4$ is summable because the real exponent $4>1$ (discharged by norm_num). Apply the natural-number shift equivalence summable_nat_add_iff with offset 1 to move the sum to $\sum 1/(n+1)^4$. Finish by a termwise congruence: after push_cast, the two real expressions agree by ring normalization. No analytic estimates beyond the classical $p$-test are used.
why it matters
This is the absolute-convergence gate for the Mellin step that turns the Bose and Fermi kernels into shifted $\zeta(4)$ and $\eta(4)$ Dirichlet series. Downstream, hasSum_mellin_bose and hasSum_mellin_fermi invoke it (via hasSum_mellin) so that
$\mathrm{mellin},F,4 = \Gamma(4)\sum a_n/(n+1)^4$
with $F$ the Bose or Fermi kernel. The same lemma is reused in RadiationEntropyRelation for the logarithmic kernels (exponent effectively 3 on the norm side, reduced by congruence to this $p=4$ fact).
With those identities in hand, uniqueness of unconditional sums closes both thermodynamic integrals and the $7/8$ ratio, so the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8 is theorem-level; only the $g^*$ species census remains model content. No Recognition forcing-chain step (T0–T8) is touched here: this is pure classical analysis supporting the cosmology bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.