bose_series
plain-language theorem explainer
For every real t > 0, the geometric series ∑_n (e^{-t})^{n+1} sums to 1/(e^t − 1). Anyone converting Bose energy or number-density integrals into zeta values via Mellin transforms cites this kernel expansion. The proof is the classical geometric HasSum at ratio e^{-t} < 1, left-multiplied by e^{-t} and rewritten by field arithmetic.
Claim. For every real $t > 0$, $\sum_{n=0}^{\infty} (e^{-t})^{n+1}$ converges unconditionally to $1/(e^{t}-1)$.
background
The module closes the gap between the series identity η(4) = (7/8)·ζ(4) and the thermodynamic statement used in entropy bookkeeping: the Fermi–Dirac energy integral equals 7/8 of the Bose–Einstein one. Both integrals are Mellin transforms at s = 4 of geometric series in e^{-t}.
The Bose kernel is the scalar function t ↦ 1/(e^t − 1) on (0, ∞). The present lemma is the series identity that feeds Mathlib's hasSum_mellin: if F(t) = ∑ a_n e^{-(n+1)t}, then mellin F s = ∑ Γ(s)·a_n/(n+1)^s. At s = 4 with Γ(4) = 6 the Dirichlet side is a shifted ζ(4), already evaluated in Cosmology.FermionWeight.
With the companion Fermi expansion and uniqueness of unconditional sums, both thermodynamic integrals evaluate in closed form (π⁴/15 and 7π⁴/120), so the 7/8 ratio is theorem-level rather than model content.
proof idea
From t > 0 one gets 0 ≤ e^{-t} < 1. Apply hasSum_geometric_of_lt_one and left-multiply by e^{-t} to obtain HasSum of n ↦ (e^{-t})^{n+1} equal to e^{-t}/(1 − e^{-t}). A short algebraic block (exp_neg, field_simp, positivity of e^t − 1) rewrites that closed form as 1/(e^t − 1). Finally congr_fun aligns the summand via pow_succ and ring.
why it matters
This is the first concrete series identity in the module derivation: both thermodynamic integrals are Mellin transforms of geometric series in e^{-t}. Downstream, hasSum_mellin_bose invokes hasSum_mellin on the Bose kernel (coefficients all 1) at s = 4, and NumberDensityIntegral.hasSum_mellin_bose3 does the same at s = 3 for the number-density layer.
Together with the Fermi twin and the already-proved η(4) = (7/8)·ζ(4) from Cosmology.FermionWeight, the module discharges the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8. Only the g* species census remains as model content. No T0–T8 forcing step is involved; the landmark is the thermodynamic 7/8 statistics factor in the entropy-per-photon chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.