bose_number_integral_value
plain-language theorem explainer
The Bose–Einstein number-density integral equals twice Apéry's constant: ∫₀^∞ t²/(eᵗ−1) dt = 2 ζ(3). Cosmologists cite it as the analytic content of the photon number density n_γ = (2ζ(3)/π²) T³. The proof is a short transport: evaluate the Mellin transform of the Bose kernel at s=3, identify it with the real integral, and inject from ℂ to ℝ.
Claim. The improper integral $\int_{0}^{\infty} \frac{t^{2}}{e^{t}-1}\,dt$ equals $2\zeta(3)$, where $\zeta(3)$ denotes Apéry's constant $\sum_{n=1}^{\infty} n^{-3}$.
background
This module closes the number-density layer (Mellin parameter s=3) for thermal cosmology, companion to the energy-density integrals at s=4. Photon number density is written n_γ = (g_γ/(2π²)) T³ ∫ t²/(eᵗ−1) dt; with g_γ=2 the integral must evaluate to 2ζ(3) to recover the textbook coefficient 2ζ(3)/π².
Apéry's constant is introduced as the real tsum ζ(3) := ∑'_{n} 1/(n+1)³ (no closed form is assumed). The Bose kernel 1/(eᵗ−1) has geometric series expansion whose Mellin transform at s=3 is Γ(3)ζ(3)=2ζ(3). Upstream, mellin_bose3_value states that complex Mellin equality, and mellin_bose3_eq_integral identifies the Mellin transform with the complexified real integral over (0,∞).
proof idea
Short term-mode transport, not a fresh evaluation. Start from mellin_bose3_value (mellin boseKernel 3 = (2·ζ(3):ℂ)). Rewrite the left-hand side by mellin_bose3_eq_integral, which equates that Mellin value to the complexification of ∫_{Ioi 0} t²/(eᵗ−1). Apply Complex.ofReal_inj to descend the equality from ℂ to ℝ. The heavy lifting (HasSum uniqueness for the Dirichlet series at s=3, Γ(3)=2) already sits in the two upstream lemmas.
why it matters
This is the last analytic ingredient of the entropy-per-photon chain at the number-density layer. Downstream, number_density_coeff_provenance rewrites g_γ·(∫t²/(eᵗ−1))/(2π²) as 2ζ(3)/π² with g_γ=2, giving provenance for n_γ=(2ζ(3)/π²)T³. fermi_div_bose_number_integral divides the Fermi number integral by this Bose value to obtain the 3/4 number-density fermion weight η(3)/ζ(3)=1−2^{-2}. entropyPerPhoton_from_integrals then expresses entropyPerPhoton exactly as a ratio of the derived thermodynamic integrals (entropy-density numerator over this photon number-density denominator), so every analytic constant in that formula is theorem-level; only particle census and statistical-mechanics identifications remain model content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.