hasSum_odd
plain-language theorem explainer
The odd-index subsum of ζ(4) equals (π⁴/90)·(15/16): ∑_k 1/(2k+1)⁴ converges unconditionally to that value. Cosmology and statistical-mechanics arguments that split Bose vs Fermi series cite it when isolating the odd part before forming η(4). The proof subtracts the even subsum from Mathlib's ζ(4) sum via HasSum.even_add_odd and uniqueness in ℝ.
Claim. The series $\sum_{k=0}^{\infty} 1/(2k+1)^4$ converges unconditionally in $\mathbb{R}$ and its sum is $(\pi^4/90)\cdot(15/16)$. Equivalently, the odd-index part of $\zeta(4)$ is $(15/16)\,\zeta(4)$.
background
The module upgrades the MODEL input fermionWeight = 7/8 in entropy-per-photon accounting to a series identity η(4) = (7/8)·ζ(4). Here ζ(4) = ∑ 1/n⁴ = π⁴/90 (Mathlib's hasSum_zeta_four), and η(4) = ∑ (−1)^{n+1}/n⁴ is the Dirichlet eta value that appears in the Fermi–Dirac integral ∫ x³/(eˣ+1) dx = Γ(4)·η(4), while the Bose–Einstein side uses ζ(4).
The derivation splits ζ(4) into even and odd indices. The even part is ∑_k 1/(2k)⁴ = (1/16)·ζ(4) by re-indexing n = 2k (the k = 0 term vanishes). That even subsum is already recorded as an unconditional HasSum. Summability of the odd terms follows by injecting k ↦ 2k+1 into the full ζ(4) series.
All sums are unconditional (HasSum over ℕ). Recombination of even and odd parts uses Mathlib's HasSum.even_add_odd; uniqueness of sums in ℝ then pins the odd total.
proof idea
Start from summability of the odd terms to obtain some real B and a HasSum witness for the odd series to B. Feed the already-proved even HasSum (value π⁴/90 / 16) and that odd witness into HasSum.even_add_odd, producing a HasSum for the full n ↦ 1/n⁴ series with value π⁴/90/16 + B.
Uniqueness against Mathlib's hasSum_zeta_four forces π⁴/90/16 + B = π⁴/90. A short linear arithmetic step rearranges to B = π⁴/90 · (15/16). Rewrite the odd witness along that equality.
why it matters
This lemma is the odd half of the even/odd split that yields η(4) = (7/8)·ζ(4). Downstream, hasSum_eta_four builds the alternating series as odd-part minus even-part and concludes η(4) = (7/8)·(π⁴/90). That identity is exactly what fermionWeight_eq_eta_zeta_ratio needs to discharge the classical eta/zeta factor from the MODEL-input list, leaving only the statistical-mechanics claim that fermions contribute the Fermi–Dirac integral.
The same subtraction pattern appears for ζ(3) in the number-density integral layer (odd part (7/8)·ζ(3), then η(3) = (3/4)·ζ(3)), so the lemma is the s = 4 instance of a reusable series template in the cosmology stack. It sits entirely at the series layer: no Recognition forcing-chain step (T0–T8) is invoked; the physics content enters only when the ratio is wired into entropy-per-photon weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.