fermi_number_integral_value
plain-language theorem explainer
The Fermi–Dirac number-density integral equals (3/2) times Apéry's constant: ∫₀^∞ t²/(eᵗ+1) dt = (3/2) ζ(3). Cosmologists cite it when building the fermionic number weight that enters n_ν/n_γ before dilution. The proof is a short real extraction: the Mellin transform of the Fermi kernel at s=3 is already (3/2)ζ(3) in ℂ and equals the real integral.
Claim. $$\int_0^\infty \frac{t^2}{e^t+1}\,dt = \frac{3}{2}\,\zeta(3),$$ where $\zeta(3)=\sum_{n=1}^\infty n^{-3}$ is Apéry's constant (as a real tsum).
background
This module closes the number-density layer (Mellin transforms at s=3) after FermionWeightIntegral closed the energy-density layer at s=4. Photon number density is written n_γ = (g_γ/(2π²)) T³ ∫ t²/(eᵗ−1) dt, so the Bose and Fermi integrals at s=3 are the last analytic inputs to entropyPerPhoton_eq_ratio.
Apéry's constant appears as zeta3 := ∑' 1/(n+1)³. The Fermi kernel 1/(eᵗ+1) has geometric series expansion whose Mellin transform at s=3 is Γ(3)·η(3). With Γ(3)=2 and the Dirichlet eta identity η(3)=(3/4)ζ(3), one expects the real integral to equal (3/2)ζ(3).
Upstream, mellin_fermi3_value already states mellin fermiKernel 3 = ((3/2)·zeta3 : ℂ), obtained by uniqueness of HasSum against the shifted eta series. mellin_fermi3_eq_integral identifies that Mellin value with the complexification of the real improper integral over Ioi 0.
proof idea
One short term-mode chain. Start from mellin_fermi3_value (mellin fermiKernel 3 equals the complexification of (3/2)zeta3). Rewrite the left-hand side via mellin_fermi3_eq_integral, which unfolds the Mellin definition and shows it equals the complexified real integral ∫_{t>0} t²/(eᵗ+1). Apply Complex.ofReal_inj to cancel the ℂ coercion and recover the real equality.
why it matters
Direct parent is fermi_div_bose_number_integral, which divides this value by the Bose companion ∫ t²/(eᵗ−1)=2ζ(3) to obtain the exact 3/4 number-density fermion weight: η(3)/ζ(3)=1−2^{-2}=3/4. That ratio is the companion of the classic 7/8 entropy weight; it dilutes fermionic number densities (e.g. n_ν/n_γ per species before e⁺e⁻ heating).
Module doc places both integrals as the final analytic ingredients of entropyPerPhoton_from_integrals, which rewrites entropyPerPhoton = π⁴ g*s/(45 ζ(3)) as a pure ratio of thermodynamic integrals. No Recognition forcing-chain step (T0–T8) is touched; the result is classical special-function input to the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.