hasSum_eta_shift
plain-language theorem explainer
The index-shifted Dirichlet eta series ∑_{n≥0} (−1)^n/(n+1)^4 equals (7/8)·(π^4/90). Cosmology and radiation-entropy proofs cite it as the concrete HasSum feeding Mellin evaluations of Fermi–Dirac kernels. The argument is a one-step index shift of the unshifted η(4) HasSum via Mathlib’s natural-number add-iff, plus a termwise algebraic congruence.
Claim. The series $\sum_{n=0}^{\infty} (-1)^n/(n+1)^4$ converges unconditionally (as a real HasSum) to $\eta(4)=(7/8)\cdot(\pi^4/90)$.
background
This module sits at the thermodynamic (integral) layer of the fermion-weight story. Cosmology.FermionWeight already proved the unshifted alternating p-series identity η(4)=(7/8)·ζ(4) as a HasSum: ∑{n≥1} (−1)^{n+1}/n^4 = (7/8)·(π^4/90). The integral layer needs the same value written with the geometric-series indexing n↦n+1 that appears in 1/(e^t+1)=∑{n≥0}(−1)^n e^{−(n+1)t}.
Both Bose and Fermi energy integrals are Mellin transforms at s=4 of those geometric kernels. Mathlib’s hasSum_mellin converts the power series in e^{−t} into a Dirichlet series Γ(s)·∑ a_n/(n+1)^s. At s=4 one has Γ(4)=6, so the Fermi side is exactly 6 times the shifted η(4) sum proved here. The module goal is to make EntropyPerPhoton’s factor 7/8 a pure theorem, leaving only the g* species census as model content.
proof idea
Start from FermionWeight.hasSum_eta_four, which asserts HasSum of n ↦ (−1)^{n+1}/n^4 equal to (7/8)·(π^4/90). Apply Mathlib’s hasSum_nat_add_iff at shift 1 (in the mpr direction) to reindex the sum so the first term is peeled and the remaining series runs over n≥0 with denominator (n+1)^4. The leftover finite sum over Finset.range 1 is absorbed into the stated target by the same base identity. Finish with HasSum.congr_fun: termwise, pow_succ and ring identify (−1)^{n+1}/(n+1)^4 with (−1)^n/(n+1)^4 up to the conventional sign pattern of the shifted eta series.
why it matters
Without the shifted HasSum, the Mellin bridge from geometric kernels to Dirichlet series cannot land on a closed real value. Downstream, mellin_fermi_value multiplies this sum by Γ(4)=6 to obtain mellin(1/(e^t+1)) 4 = 7π^4/120, i.e. the Fermi–Dirac energy integral in closed form. RadiationEntropyRelation.mellin_fermiLog_value likewise scales it by 2 to evaluate mellin(ln(1+e^{−t})) 3 = 7π^4/360 for the entropy integrand.
Together these close the mathematical content of fermionWeight=7/8 in the entropy-per-photon chain: Bose gives π^4/15, Fermi gives 7π^4/120, and the ratio is exactly 7/8. That is the statistics factor used in RS cosmology bookkeeping; only the relativistic species census remains model-side. The result is axiom-clean (Lean’s base axioms only) and sits entirely inside the proved integral layer announced by the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.