fermiLog_integral_value
plain-language theorem explainer
The improper integral ∫₀^∞ t² ln(1+e^{-t}) dt equals 7π⁴/360. Cosmology and quantum-statistics workers cite it as the closed form of the Fermi–Dirac logarithmic kernel that appears when the entropy integrand splits into energy plus log pieces. The proof is a short bridge: the Mellin transform of that kernel at order 3 is already 7π⁴/360, and a companion identity equates the Mellin value to the complexified real integral, so real embedding injectivity finishes it.
Claim. $$\int_0^\infty t^2 \ln(1+e^{-t})\,dt = \frac{7\pi^4}{360}.$$
background
The radiation-entropy module derives the thermodynamic relation $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional, rather than taking the $4/3$ factor as an external input. For Fermi–Dirac statistics the entropy integrand splits pointwise into the energy kernel $t^3/(e^t+1)$ plus the logarithmic kernel $t^2\ln(1+e^{-t})$.
That log piece is evaluated by Mellin methods. Upstream, the Mellin transform of the Fermi log kernel at order 3 equals $\Gamma(3)\eta(4)=7\pi^4/360$, obtained from the alternating eta series. A companion lemma identifies the same Mellin value with the complexification of the real improper integral on $(0,\infty)$. The present theorem simply recovers the real equality.
proof idea
Take the already-proved Mellin evaluation: the Mellin transform of the Fermi log kernel at $3$ equals the complex number $7\pi^4/360$. Rewrite that identity by the companion lemma that equates the Mellin transform to the complexification of $\int_{(0,\infty)} t^2\ln(1+e^{-t}),dt$. Apply injectivity of the real-to-complex embedding to descend to the real equality. Three steps, no new analysis.
why it matters
This is the log-channel half of the Fermi entropy integral. Combined with the energy integral it yields $\int\sigma_F=7\pi^4/90$, which is exactly $(4/3)$ times the Fermi energy integral and places the fermionic $7/8$ weight at the entropy-functional layer (not only at the energy layer). Downstream, the plasma-pressure theorem uses the same closed form (with the Bose counterpart $\pi^4/45$) to collapse pressure to $P=(\pi^2/90)(g_B+(7/8)g_F)T^4$, so the $7/8$ factor emerges independently in the pressure channel. It also witnesses integrability of the Fermi log kernel, since the integral is nonzero. In the broader $\eta_B$ chain the module closes the MODEL identification $s=(4/3)\rho/T$ without assuming the thermodynamic factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.