summable_odd
plain-language theorem explainer
The series of reciprocal fourth powers over odd positive integers is summable on ℕ. Cosmology proofs that split ζ(4) into even and odd subseries cite this to obtain an unconditional HasSum for the odd part. The argument pulls summability of n ↦ n^{-4} back along the injective reindexing k ↦ 2k+1 and rewrites the composition.
Claim. The real series $\sum_{k=0}^{\infty} 1/(2k+1)^4$ is summable.
background
This module upgrades the cosmology input fermionWeight = 7/8 to a derived series identity η(4) = (7/8)·ζ(4). Here ζ(4) = ∑_{n≥1} n^{-4} = π⁴/90 (Mathlib hasSum_zeta_four), and η(4) is the Dirichlet eta value that enters the Fermi–Dirac integral ∫ x³/(eˣ+1) dx = Γ(4)·η(4), while the Bose–Einstein side uses ζ(4).
The derivation splits ζ(4) into even-index and odd-index parts: even terms reindex as (1/16)·ζ(4), and the odd part is the complementary (15/16)·ζ(4). Alternating recombination then yields η(4) = odd − even = (7/8)·ζ(4). All sums are unconditional HasSum over ℕ.
Before assigning a numerical value to the odd subsum, one needs summability of k ↦ (2k+1)^{-4}. That is the present lemma. An identical pattern appears for the cubic series in NumberDensityIntegral (power 3 instead of 4).
proof idea
Start from summability of the full zeta series: hasSum_zeta_four.summable gives Summable (n ↦ n^{-4}).
Prove injectivity of the odd reindexing φ(k) = 2k+1 by a short omega argument on natural numbers.
Apply Summable.comp_injective to pull summability back along φ, then Summable.congr with Function.comp_apply to match the stated term (2k+1)^{-4}. No value is computed; only existence of the sum is established.
why it matters
Immediate consumer is hasSum_odd in the same module, which obtains ∑_k (2k+1)^{-4} = (π⁴/90)·(15/16) by subtracting the even part from the full zeta sum and using uniqueness of unconditional real sums. That odd HasSum is the missing half of the even/odd split that produces η(4) = (7/8)·ζ(4).
The terminal theorem fermionWeight_eq_eta_zeta_ratio then identifies the rational 7/8 used in EntropyPerPhoton.fermionWeight with the classical eta/zeta ratio, removing that identity from the MODEL-input list. Only the statistical-mechanics claim (fermions contribute the Fermi–Dirac integral) remains as physics input.
A parallel summable_odd for power 3 in NumberDensityIntegral uses the same injective-composition pattern, so this lemma is the fourth-power instance of a reusable series-layer technique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.