mellin_fermiLog_value
plain-language theorem explainer
The Mellin transform of the Fermi logarithmic kernel ln(1+e^{-t}) at s=3 equals 7π⁴/360 in ℂ. Anyone closing the Fermi half of the radiation entropy identity s=(4/3)ρ/T from the microscopic entropy functional cites this evaluation. The proof matches the Mellin series to twice the shifted Dirichlet eta series at weight 4 and invokes uniqueness of HasSum.
Claim. The Mellin transform of the Fermi logarithmic kernel $t\mapsto\ln(1+e^{-t})$ at $s=3$ equals $7\pi^4/360$ as a complex value: $\mathcal{M}[\ln(1+e^{-t})](3)=\Gamma(3)\,\eta(4)=7\pi^4/360$.
background
This module derives the thermodynamic relation $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional, rather than assuming the $4/3$ factor. For Fermi–Dirac statistics the entropy integrand splits pointwise as $\sigma_F(x)=x^3/(e^x+1)+x^2\ln(1+e^{-x})$; the second summand is the logarithmic pressure kernel.
The complex-valued Fermi logarithmic kernel is $\mathrm{fermiLogKernel}(t)=\ln(1+e^{-t})$ (cast $\mathbb{R}\to\mathbb{C}$). Its Mellin transform at integer order $s=3$ is the series $\Gamma(3)\sum_{n\ge0}(-1)^n(n+1)^{-4}$, i.e. $\Gamma(3)\eta(4)$. Upstream, $\Gamma(3)=2$ and the shifted eta sum $\sum(-1)^n/(n+1)^4=(7/8)(\pi^4/90)$ are already available, so the closed value is $2\cdot7\pi^4/720=7\pi^4/360$.
The companion Bose evaluation at the same order yields $4\pi^4/360=\pi^4/90$; the ratio of the two log integrals recovers the $7/8$ fermionic weight at the entropy-functional layer.
proof idea
Uniqueness of HasSum is applied to the already-established series representation hasSum_mellin_fermiLog. It remains only to exhibit a concrete HasSum for the coefficient series equal to $7\pi^4/360$.
Start from hasSum_eta_shift (the real sum $\sum(-1)^n/(n+1)^4=(7/8)(\pi^4/90)$) and multiply on the left by $2$; a one-line ring conversion identifies the target real sum. Lift to $\mathbb{C}$ by Complex.hasSum_ofReal. Congruence of summands then rewrites each term via gamma_three ($\Gamma(3)=2$) and cpow_shift3 (complex power $(n+1)^3$ equals the real cube cast), followed by field_simp after a nonzero denominator check on $n+1$.
why it matters
Downstream, fermiLog_integral_value converts this Mellin identity into the real improper integral $\int_0^\infty t^2\ln(1+e^{-t}),dt=7\pi^4/360$ by equating Mellin transform and integral. That integral is exactly the logarithmic half of the Fermi entropy functional, so together with the energy-kernel evaluation it yields $\int\sigma_F=7\pi^4/90=(4/3)\int x^3/(e^x+1)$ without assuming the thermodynamic $4/3$.
In the broader $\eta_B$ chain this closes the MODEL step that previously treated $s=(4/3)\rho/T$ as an external statistical-mechanics input. The same value feeds the entropy-layer $7/8$ ratio fermi_div_bose_entropy and the coefficient $2\pi^2/45$ of $s_\gamma$. No Recognition forcing-chain landmark (T5–T8, RCL, $\phi$) is invoked here; the result is pure analytic number theory in service of the cosmology entropy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.