hasSum_mellin_fermiLog
plain-language theorem explainer
The Mellin transform of the Fermi log kernel ln(1+e^{-t}) at s=3 equals the Dirichlet series Γ(3)∑(-1)^n(n+1)^{-4}. Cosmology proofs that close the fermionic entropy integral cite this identity. The argument feeds the Mercator expansion and norm-summability into the generic Mellin–Dirichlet interchange lemma at s=3.
Claim. The series $n \mapsto \Gamma(3)\,(-1)^n(n+1)^{-4}$ (as a complex sequence) has sum equal to the Mellin transform $\mathcal{M}\{\ln(1+e^{-t})\}(3)$.
background
This module derives the radiation identity $s=(4/3)\rho/T$ from the microscopic entropy functional of a massless quantum gas, rather than assuming the thermodynamic factor. For Fermi–Dirac statistics the entropy integrand splits pointwise into the energy kernel plus a logarithmic kernel $\ln(1+e^{-x})$.
The Fermi logarithmic kernel is the complexification of $\ln(1+e^{-t})$. Its Mercator series on $t>0$ is $\ln(1+e^{-t})=\sum_{n\ge 0}(-1)^n e^{-(n+1)t}/(n+1)$ (fermiLog_series). The companion summability lemma bounds $|(-1)^n/(n+1)|/(n+1)^3$, which is the $s=3$ hypothesis needed to interchange Mellin transform and series.
The generic tool is a Mellin–Dirichlet identity: if $F(t)=\sum a_n e^{-p_n t}$ with suitable positivity and summability, then $\mathcal{M}{F}(s)=\Gamma(s)\sum a_n p_n^{-s}$.
proof idea
One application of the generic hasSum_mellin lemma with coefficients $a_n=(-1)^n/(n+1)$, scales $p_n=n+1$, kernel $F=$ Fermi log kernel, and $s=3$. Positivity of the scales and $s=3\neq 0$ are discharged by positivity/norm_num.
The pointwise series hypothesis is the complexification of fermiLog_series: after rewriting $\exp(-(n+1)t)=\exp(-t)^{n+1}$, the terms match by ring. Absolute summability is exactly summable_norm_fermiLog.
why it matters
Feeds directly into mellin_fermiLog_value, which evaluates the Mellin transform as $\Gamma(3)\eta(4)=7\pi^4/360$. That closed form is the fermionic half of the entropy-functional computation: integrating the log kernel against $x^2$ yields the missing piece that turns the energy integral into $\int\sigma_F=7\pi^4/90=(4/3)$ times the Fermi energy integral.
Together with the Bose twin, this closes the MODEL step that previously treated $s=(4/3)\rho/T$ as thermodynamic input in the $\eta_B$ chain (EntropyPerPhoton, NumberDensityIntegral). The $7/8$ fermionic weight then holds at the entropy-functional layer, not only at the energy layer. No Recognition forcing-chain landmark (T5–T8) is invoked here; the result is classical analytic number theory inside the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.