fermi_integral_value
plain-language theorem explainer
The Fermi–Dirac energy integral equals 7π⁴/120 in closed form. Anyone deriving radiation energy density, entropy per photon, or the 7/8 fermion weight at the thermodynamic layer cites this evaluation. The proof is a short transport: the Mellin value at s=4 is already known, rewritten as the real integral, then recovered by injectivity of real-to-complex coercion.
Claim. The improper integral of the massless Fermi–Dirac energy kernel equals a multiple of $\pi^4$: $\int_0^\infty t^3/(e^t+1)\,dt = 7\pi^4/120$.
background
This module sits at the thermodynamic layer of the fermion-weight story. Earlier work in FermionWeight proved the Dirichlet identity $\eta(4)=(7/8)\zeta(4)$. The remaining gap is to identify the physical energy integrals with those series via Mellin transforms.
For $t>0$, the Fermi kernel expands as $1/(e^t+1)=\sum_{n\ge 0}(-1)^n e^{-(n+1)t}$. Mathlib's Mellin-of-power-series lemma converts that expansion at $s=4$ into $\Gamma(4)\cdot\eta(4)$. With $\Gamma(4)=6$ and the known value of the shifted eta sum, one obtains the complex Mellin value $7\pi^4/120$.
Upstream, mellin_fermi_value states that the Mellin transform of the Fermi kernel at 4 equals that constant in $\mathbb{C}$, and mellin_fermi_eq_integral identifies the Mellin transform with the complexification of the real integral $\int_{(0,\infty)} t^3/(e^t+1),dt$.
proof idea
Three-line term proof. Start from mellin_fermi_value, which gives mellin fermiKernel 4 = (7π⁴/120 : ℝ) : ℂ. Rewrite the left side by mellin_fermi_eq_integral, so the complexified real integral equals that constant. Finish with Complex.ofReal_inj.mp to drop the complex embedding and recover the real equality.
why it matters
This is the closed-form Fermi half of the integral-layer 7/8 theorem. Immediately downstream, fermi_div_bose_integral divides by the Bose value $\pi^4/15$ to get exactly 7/8, and fermi_integral_eq_weight_mul_bose identifies that ratio with the MODEL constant EntropyPerPhoton.fermionWeight. The module header records the payoff: the entire mathematical content of the 7/8 factor is then THEOREM; only the $g^*$ species census remains MODEL.
Further parents use the constant directly: plasmaEnergy_eq assembles $\rho=(\pi^2/30)(g_B+(7/8)g_F)T^4$; the radiation-entropy chain evaluates the Fermi entropy integral and the $s=(4/3)\rho/T$ law for fermions; integrability of the Fermi energy kernel is proved by contradiction against the nonzero value $7\pi^4/120$. In the broader RS cosmology bookkeeping this pins the statistics factor that multiplies fermionic degrees of freedom in early-universe entropy and energy densities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.