fermi_entropy_integral_value
plain-language theorem explainer
The Fermi–Dirac entropy integral equals 7π⁴/90: ∫₀^∞ t²[−f ln f − (1−f)ln(1−f)] dt with f=1/(eᵗ+1). Cosmologists deriving s=(4/3)ρ/T or the 7/8 fermionic weight from the microscopic entropy functional cite this value. The proof splits the integrand pointwise into the energy kernel plus a log kernel, integrates termwise, and adds 7π⁴/120 + 7π⁴/360.
Claim. With $f(t)=1/(e^t+1)$, the Fermi–Dirac entropy integral evaluates exactly to $$\int_0^\infty t^2\bigl[-f\ln f-(1-f)\ln(1-f)\bigr]\,dt=\frac{7\pi^4}{90}.$$
background
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. Dimensionless integrals use $t=E/T$. The Fermi entropy integrand is $\sigma_F(t)=t^2[-f\ln f-(1-f)\ln(1-f)]$ with occupation $f=1/(e^t+1)$.
A pointwise identity decomposes $\sigma_F$ on $(0,\infty)$ into the Fermi energy kernel plus a logarithmic kernel: $\sigma_F(t)=t^3/(e^t+1)+t^2\ln(1+e^{-t})$. The energy piece integrates to $7\pi^4/120$ (Fermi–Dirac integral from FermionWeightIntegral). The log piece integrates to $7\pi^4/360$ (via a Mellin evaluation of the series for $\ln(1+e^{-t})$). Both kernels are integrable on $(0,\infty)$, justified by contradiction against those nonzero closed forms.
proof idea
Rewrite the integral by the pointwise Fermi decomposition: on $(0,\infty)$, the entropy integrand equals $t^3/(e^t+1)+t^2\ln(1+e^{-t})$. Congruence of integrands on Ioi 0 yields equality of integrals. Split the sum with integral_add, using integrability of each kernel. Substitute the closed forms $7\pi^4/120$ (Fermi energy integral) and $7\pi^4/360$ (Fermi log integral). Finish by ring: $7/120+7/360=7/90$.
why it matters
This is the Fermi half of the module's main evaluation pair. It feeds four parents: the structural plasma formula radiationEntropy_eq, which collapses $s$ to $(2\pi^2/45)(g_B+(7/8)g_F)T^3$ with both the prefactor and the 7/8 weight derived; fermi_entropy_eq_four_thirds_energy, the Fermi $s=(4/3)\rho/T$ law; fermi_div_bose_entropy, the 7/8 ratio at the entropy-functional layer; and fermi_entropy_eq_weight_mul_bose, tying the integral to the MODEL constant fermionWeight.
In the broader η_B chain this closes a former thermodynamic assumption: entropy-per-photon and number-density work previously imported 4/3 and 7/8; here both emerge from $\sigma_F$ and $\sigma_B$. No Recognition forcing landmark (T5–T8, RCL) is invoked; the result is pure statistical-mechanics input to the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.