bose_entropy_eq_four_thirds_energy
plain-language theorem explainer
For a massless Bose gas the dimensionless entropy integral equals exactly four-thirds the Bose energy integral, giving the thermodynamic law s = (4/3) ρ/T without assuming it. Cosmologists tracking the η_B entropy chain and radiation thermodynamics cite this. The proof rewrites both sides to closed π⁴ values and finishes by ring arithmetic.
Claim. Let $\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr]$ with $f=1/(e^t-1)$. Then $\int_0^\infty \sigma_B(t)\,dt = \frac{4}{3}\int_0^\infty \frac{t^3}{e^t-1}\,dt$.
background
This module derives the radiation identity $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional of quantum statistics, rather than taking the $4/3$ factor as a thermodynamic input. Earlier links in the entropy chain (entropy per photon, number-density integrals) used that factor as an assumption; here it is proved.
The Bose entropy integrand is $\sigma_B(t)=t^2\bigl[(1+f)\ln(1+f)-f\ln f\bigr]$ with occupation $f=1/(e^t-1)$. A pointwise split writes $\sigma_B$ as the energy kernel $t^3/(e^t-1)$ plus a logarithmic kernel $t^2(-\ln(1-e^{-t}))$. The energy side is the classical Bose–Einstein integral $\int_0^\infty t^3/(e^t-1),dt=\pi^4/15$. The entropy integral evaluates to $4\pi^4/45$.
The present statement is the dimensionless content of $s=(4/3)\rho/T$: once both integrals are known, the ratio is exactly $4/3$.
proof idea
One-line algebraic comparison of two closed forms. Rewrite the left-hand side by bose_entropy_integral_value, which supplies $\int\sigma_B=4\pi^4/45$. Rewrite the energy integral by bose_integral_value, which supplies $\int t^3/(e^t-1),dt=\pi^4/15$. Then ring checks $4\pi^4/45=(4/3)\cdot(\pi^4/15)$. No further analytic work is done at this site; the hard integral evaluations live upstream.
why it matters
Closes a MODEL step in the baryon-asymmetry entropy chain: the statistical-mechanics identification $s=(4/3)\rho/T$ for massless bosons is now a theorem from the entropy functional, not an imported thermodynamic axiom. The module status is fully proved (zero sorry). The companion Fermi statement and the $7/8$ entropy-weight ratio sit beside it, so the fermionic statistics factor holds at the entropy-functional layer as well as the energy layer. The entropy coefficient $2\pi^2/45$ in $s_\gamma=(2\pi^2/45)g T^3$ then emerges without ever inserting $4/3$ by hand. No downstream consumers are wired yet in the graph; the immediate audience is the radiation-era bookkeeping that feeds $\eta_B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.