integrableOn_fermiLog

This module derives the radiation identity $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional, rather than assuming the thermodynamic $4/3$ factor. For Fermi–Dirac statistics the entropy integrand splits pointwise as

$$\sigma_F(t)=\frac{t^{3}}{e^{t}+1}+t^{2}\log(1+e^{-t}),$$

so the logarithmic piece $t^{2}\log(1+e^{-t})$ must be handled separately from the energy kernel.

Upstream, the Mellin-transform evaluation already supplies the definite integral $\int_{0}^{\infty}t^{2}\log(1+e^{-t}),dt=7\pi^{4}/360$. Integrability on $(0,\infty)$ is the missing analytic hypothesis that lets that equality be used inside Lebesgue integral calculus (congruence, additivity, comparison with the energy integral).

Proof by contradiction. Assume the map is not integrable on $(0,\infty)$. Then Mathlib’s integral_undef forces the Lebesgue integral over that set to equal $0$. Rewrite that vanishing statement with the already-proved closed form fermiLog_integral_value, obtaining $7\pi^{4}/360=0$. A positivity check gives $0<7\pi^{4}/360$, and linarith closes the contradiction. No series expansion or dominated-convergence argument is reopened here; the lemma only harvests the nonzero closed form.

Downstream, fermi_entropy_integral_value splits the Fermi entropy integrand into energy kernel plus this logarithmic kernel and adds the two integrals. Without integrability of the log piece, that sum is not justified as a real number, and the closed form $\int\sigma_F=7\pi^{4}/90$ fails.

That value is half of the module’s main claim: $\int\sigma_F=(4/3)\int t^{3}/(e^{t}+1)$, which installs the factor $4/3$ at the entropy-functional layer for fermions and yields the $7/8$ entropy weight relative to bosons. In the broader $\eta_B$ chain this closes a MODEL gap that earlier entropy-per-photon work treated as thermodynamic input.