mellin_fermi_value
plain-language theorem explainer
The Mellin transform of the Fermi–Dirac kernel 1/(e^t+1) at s=4 equals 7π⁴/120 in ℂ, equivalently Γ(4)·η(4). Anyone closing the thermodynamic Fermi integral or the 7/8 fermion weight cites this evaluation. The proof matches the Mellin/Dirichlet series to a scaled η(4) sum and invokes uniqueness of unconditional sums.
Claim. The Mellin transform of the Fermi–Dirac kernel $1/(e^{t}+1)$ at $s=4$ equals $7\pi^{4}/120$ as a complex number: $\mathcal{M}\{1/(e^{t}+1)\}(4)=\Gamma(4)\,\eta(4)=7\pi^{4}/120$.
background
This module sits at the integral (thermodynamic) layer of the fermion-weight chain. The series identity η(4)=(7/8)ζ(4) is already available from Cosmology.FermionWeight; the remaining gap is to identify the Fermi–Dirac energy integral ∫₀^∞ t³/(e^t+1) dt with a closed form. Both Bose and Fermi kernels expand as geometric series in e^{-t} for t>0, and the Mellin transform of such a series is a Dirichlet series: mellin F s = ∑_n Γ(s) a_n/(n+1)^s.
Here fermiKernel is the complexification of 1/(e^t+1). The upstream lemma hasSum_mellin_fermi states that mellin fermiKernel 4 is the sum of Γ(4)·(-1)^n/(n+1)^4. Gamma at 4 is 3!=6 (gamma_four), and the shifted alternating fourth-power sum is η(4)=(7/8)(π⁴/90) (hasSum_eta_shift). The companion cpow_shift lemma equates complex and real fourth powers on positive reals so the Dirichlet terms match after casting.
proof idea
Uniqueness of HasSum is the spine: refine hasSum_mellin_fermi.unique, so it remains only to exhibit a real series that sums to 7π⁴/120 and agrees termwise with the complex Mellin/Dirichlet sum.
Scale hasSum_eta_shift by 6 (from Γ(4)=6) to get HasSum of 6·(-1)^n/(n+1)^4 equal to 7π⁴/120; a ring conversion aligns the target constant. Lift that real HasSum into ℂ via Complex.hasSum_ofReal. Termwise congruence then rewrites each complex summand with gamma_four and cpow_shift, followed by push_cast and ring, matching Γ(4)·(-1)^n/(n+1)^{4:ℂ}.
why it matters
Downstream, fermi_integral_value quotes this lemma, rewrites the Mellin value as the improper real integral via mellin_fermi_eq_integral, and concludes ∫₀^∞ t³/(e^t+1) dt = 7π⁴/120. That closed form is the Fermi half of the thermodynamic identity
∫ t³/(e^t+1) = (7/8)·∫ t³/(e^t−1),
with Bose side π⁴/15. Module documentation records that once both Mellin evaluations are theorems, the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8 is theorem-status: only the g* species census remains model content. In the Recognition cosmology bookkeeping this fixes the fermionic contribution to the entropy-per-photon factor without residual analytic gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.