entropy_coeff_from_functional
plain-language theorem explainer
The Bose–Einstein entropy integral, divided by the phase-space factor 2π², equals exactly 2π²/45. Cosmologists and RS auditors cite this for the photon entropy density prefactor s_γ=(2π²/45)·g·T³ without assuming the thermodynamic 4/3 relation. The proof rewrites via the known integral value 4π⁴/45 and clears the denominator by ring algebra.
Claim. The integral of the Bose–Einstein entropy integrand $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with $f=1/(e^t-1)$ over $(0,\infty)$, divided by $2\pi^2$, equals $2\pi^2/45$.
background
This module derives the radiation entropy relation $s=(4/3)\rho/T$ from the microscopic entropy functional of quantum statistics, rather than taking 4/3 as a thermodynamic input. For dimensionless energy $t=E/T$, the Bose entropy integrand is $\sigma_B(t)=t^2[(1+f)\ln(1+f)-f\ln f]$ with occupation $f=1/(e^t-1)$.
Upstream, that integrand integrates to $4\pi^4/45$ over the positive reals. The evaluation splits $\sigma_B$ pointwise into the energy kernel $t^3/(e^t-1)$ plus a logarithmic kernel and sums the resulting Mellin series. The factor $2\pi^2$ is the standard phase-space normalization that converts the dimensionless integral into the coefficient of a physical photon entropy density.
proof idea
Short tactic proof. Rewrite the numerator by the already-proved evaluation $\int_0^\infty\sigma_B=4\pi^4/45$. Clear division by $2\pi^2$ using the field identity (denominator positive by positivity). Finish with ring: $(4\pi^4/45)/(2\pi^2)=2\pi^2/45$.
why it matters
Closes the entropy-coefficient extraction in the radiation entropy chain of the η_B program. Module status is THEOREM with zero sorry: the classical prefactor $2\pi^2/45$ in $s_\gamma=(2\pi^2/45),g,T^3$ emerges from the entropy functional, and the 4/3 factor is never assumed. It sits with the Bose and Fermi four-thirds identities and the 7/8 fermionic entropy weight proved in the same file. No downstream used_by edges are recorded yet; the declaration is the terminal Bose-sector coefficient step that earlier entropy-per-photon work had taken as input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.