entropy_density_coeff_provenance
plain-language theorem explainer
The classical radiation entropy-density prefactor 2π²/45 equals (4/3) times the normalized Bose energy integral ∫t³/(eᵗ−1) dt over 2π². Cosmologists tracking the provenance of s = (2π²/45) g_*s T³ cite this identity. The proof substitutes the known Bose–Einstein value π⁴/15 and finishes by field arithmetic.
Claim. $$\frac{4}{3}\cdot\frac{\displaystyle\int_{0}^{\infty} t^{3}/(e^{t}-1)\,dt}{2\pi^{2}} = \frac{2\pi^{2}}{45}.$$ Equivalently, the coefficient in $s=(2\pi^{2}/45)\,g_{*s}T^{3}$ is exactly the radiation identity $s=(4/3)\rho/T$ applied to the Bose energy integral with the standard phase-space normalization $1/(2\pi^{2})$.
background
This module sits in the number-density integral layer of RS cosmology. The companion module closed the energy-density Mellin transforms at $s=4$; here the focus is $s=3$ and the analytic constants that feed the entropy-per-photon ratio.
The Bose–Einstein energy integral is already a theorem upstream: $\int_{0}^{\infty} t^{3}/(e^{t}-1),dt=\pi^{4}/15$. In radiation thermodynamics one has $s=(4/3)\rho/T$. With the usual phase-space factor $1/(2\pi^{2})$, the entropy-density coefficient is therefore $(4/3)$ times that integral divided by $2\pi^{2}$. The classical closed form of the same coefficient is $2\pi^{2}/45$ in $s=(2\pi^{2}/45),g_{*s}T^{3}$.
The module doc frames this identity as part of rewriting entropyPerPhoton as a pure ratio of derived thermodynamic integrals, leaving only the particle census and statistical-mechanics identifications as model content.
proof idea
One short algebraic proof. Rewrite the integral by the upstream theorem bose_integral_value, which supplies $\int_{0}^{\infty} t^{3}/(e^{t}-1),dt=\pi^{4}/15$. Record $\pi\neq 0$, then field_simp clears the denominators $2\pi^{2}$ and $15$. A final ring reduces both sides to the common rational multiple of $\pi^{2}$. No series or Mellin work is redone here; all analytic content is inherited from the energy-integral theorem.
why it matters
In the RS cosmology stack this pins the provenance of the textbook coefficient $2\pi^{2}/45$: it is not an independent input but the radiation relation $s=(4/3)\rho/T$ applied to the proved Bose energy integral. The next declaration in the file (entropy per photon from the thermodynamic integrals) uses exactly this numerator, pairing it with the photon number-density coefficient built from $\int t^{2}/(e^{t}-1)$, so that every analytic constant in the entropy-per-photon chain is theorem-grade.
That closes the integral layer of $s/n_{\gamma}=\pi^{4} g_{*s}/(45\zeta(3))$ with $g_{*s}=43/11$. Remaining model content is the species census and the statistical-mechanics dictionary, not the special-function identities. No downstream dependents are recorded yet; the declaration is a local provenance lemma for the entropy-density side of that ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.