number_density_coeff_provenance
plain-language theorem explainer
The standard photon number-density prefactor 2ζ(3)/π² equals g_γ times the Bose integral ∫₀^∞ t²/(eᵗ−1) dt, normalized by 2π², with g_γ = 2. Anyone writing n_γ = (2ζ(3)/π²) T³ from first principles cites this provenance. The proof substitutes the evaluated Bose number integral and cancels with g_γ = 2 by field arithmetic.
Claim. With photon internal degrees of freedom $g_\gamma = 2$, $$g_\gamma \cdot \frac{1}{2\pi^2}\int_0^\infty \frac{t^2}{e^t-1}\,dt = \frac{2\zeta(3)}{\pi^2},$$ where $\zeta(3)$ is Apéry's constant $\sum_{n\ge 1} n^{-3}$.
background
This module closes the number-density layer (Mellin transforms at $s=3$) for thermal radiation. The companion energy-density integrals live at $s=4$ in FermionWeightIntegral. The target identity is the analytic content of
$$n_\gamma = \frac{g_\gamma}{2\pi^2} T^3 \int_0^\infty \frac{t^2}{e^t-1},dt = \frac{2\zeta(3)}{\pi^2} T^3.$$
Here $g_\gamma = 2$ is the photon polarization count (a model input), and $\zeta(3)$ is Apéry's constant as the real tsum $\sum 1/(n+1)^3$. The Bose number integral itself is already evaluated upstream: $$\int_0^\infty \frac{t^2}{e^t-1},dt = 2\zeta(3),$$ via the Mellin–Dirichlet argument at $s=3$ with $\Gamma(3)=2$.
The same module also treats the Fermi kernel, yielding the number-density fermion weight $\eta(3)/\zeta(3)=3/4$, the companion of the $7/8$ entropy weight.
proof idea
One-line algebraic provenance, not a new integral evaluation.
- Rewrite the integral by
bose_number_integral_value, replacing $\int t^2/(e^t-1),dt$ with $2\zeta(3)$. - Unfold $g_\gamma$ to the rational $2$.
- Record $\pi\ne 0$, push casts from $\mathbb{Q}$ to $\mathbb{R}$, and finish by
field_simp.
No series or measure-theoretic work happens here; that is already sealed in the Mellin layer behind bose_number_integral_value.
why it matters
Pins the textbook coefficient of $n_\gamma=(2\zeta(3)/\pi^2)T^3$ to the Bose number integral and the phase-space factor $1/(2\pi^2)$, with $g_\gamma=2$ explicit. The module doc identifies the $s=3$ number-density layer as the last analytic ingredient of the entropyPerPhoton ratio formula
$$\frac{s}{n_\gamma}=\frac{\pi^4 g_{*s}}{45\zeta(3)}.$$
Together with the entropy-density coefficient provenance (the $2\pi^2/45$ factor from $s=(4/3)\rho/T$ and the $s=4$ Bose energy integral), this supplies both halves of that ratio from integrals rather than by citation. No downstream Lean consumers are wired yet (used_by empty), but the declaration is the natural bridge from the integral layer into cosmological number-density bookkeeping and neutrino-to-photon ratios before dilution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.