entropyPerPhoton_from_integrals
plain-language theorem explainer
The present-day entropy per photon equals the ratio of the Bose entropy-density coefficient (4/3 times the Mellin integral of t³/(eᵗ−1) over 2π², times g*s) to the Bose number-density coefficient (g_γ times the Mellin integral of t²/(eᵗ−1) over 2π²). Cosmologists equating s/n_γ to the classical π⁴ g*s/(45 ζ(3)) form cite this identity. The proof substitutes the two closed Bose Mellin values and cancels algebraically.
Claim. The entropy per photon equals $\bigl(\tfrac{4}{3}\cdot(\int_{0}^{\infty} t^{3}/(e^{t}-1)\,dt)/(2\pi^{2})\cdot g_{*s}\bigr)\big/\bigl(g_{\gamma}\cdot(\int_{0}^{\infty} t^{2}/(e^{t}-1)\,dt)/(2\pi^{2})\bigr)$, where $g_{*s}$ is the present-day entropy effective degrees of freedom and $g_{\gamma}=2$ counts photon polarizations.
background
This module closes the number-density layer of thermal integrals at Mellin weight $s=3$. The Bose kernel gives $\int_{0}^{\infty} t^{2}/(e^{t}-1),dt=\Gamma(3)\zeta(3)=2\zeta(3)$, so the photon number density is $n_{\gamma}=(g_{\gamma}/(2\pi^{2}))T^{3}\cdot 2\zeta(3)$. The companion Fermi integral yields the number-density fermion weight $\eta(3)/\zeta(3)=3/4$.
Upstream, entropyPerPhoton is defined as $\pi^{4}\cdot(43/11)/(45\zeta(3))$, with $g_{*s}=43/11$ proved from photons plus three neutrino species diluted by $(T_{\nu}/T_{\gamma})^{3}=4/11$, and $g_{\gamma}=2$. The energy-density companion module already evaluated the $s=4$ Bose integral that supplies the entropy-density factor via $s=(4/3)\rho/T$.
The local goal is to rewrite the closed-form entropy-per-photon ratio purely in terms of the two derived thermodynamic integrals, so every analytic constant in the chain is a theorem and only the particle census remains model input.
proof idea
Term-mode proof. Rewrite the two Mellin integrals by the already-proved evaluations: the $s=4$ Bose integral (energy/entropy density) and the $s=3$ Bose number-density integral of this module. Replace $g_{*s}$ by its rational value $43/11$. Unfold the definition of entropy per photon and of $g_{\gamma}$. After casting rationals to reals, field_simp clears the nonzero denominators $\pi$ and $\zeta(3)$ (the latter from positivity of Apéry's constant), and ring finishes the algebraic identity.
why it matters
Capstone of the number-density integral module and the last analytic step of the entropy-per-photon chain. The module doc states that this declaration rewrites the whole $\pi^{4} g_{*s}/(45\zeta(3))$ ratio as a ratio of the two derived thermodynamic integrals, so every analytic constant is now theorem; remaining model content is only the particle census and the statistical-mechanics identifications.
No downstream Lean consumers are recorded yet. In the broader Recognition cosmology stack it supplies the clean integral form of $s/n_{\gamma}$ that later numerical or RS-ladder comparisons can quote without reopening $\zeta(3)$ or the Bose Mellin transforms. It does not itself touch the forcing chain (T0–T8), $\phi$, or $\alpha$; it is pure thermal-field-theory bookkeeping inside the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.