hasSum_eta_four
plain-language theorem explainer
The Dirichlet eta series at 4 converges unconditionally to (7/8)·(π⁴/90), i.e. η(4)=(7/8)·ζ(4). Cosmology and statistical-mechanics arguments that need the Fermi–Dirac weight cite this as the series-level source of the classical 7/8 factor. The proof recombines even- and odd-index HasSums via Mathlib's even_add_odd after simplifying the alternating signs.
Claim. The series $\sum_{n=0}^{\infty} (-1)^{n+1}/n^4$ (with the $n=0$ term read as zero in $\mathbb{R}$) converges unconditionally, and its sum is $\frac{7}{8}\cdot\frac{\pi^4}{90}$. Equivalently, $\eta(4)=\frac{7}{8}\,\zeta(4)$ with $\zeta(4)=\pi^4/90$.
background
The module upgrades the MODEL constant fermionWeight = 7/8 used in entropy-per-photon bookkeeping to a derived series identity. In thermal field theory the Bose–Einstein integral $\int_0^\infty x^3/(e^x-1),dx$ equals $\Gamma(4),\zeta(4)$, while the Fermi–Dirac integral $\int_0^\infty x^3/(e^x+1),dx$ equals $\Gamma(4),\eta(4)$. The ratio of those weights is therefore $\eta(4)/\zeta(4)$.
Here $\zeta(4)=\sum 1/n^4=\pi^4/90$ is Mathlib's hasSum_zeta_four. The even-index subsum is $\sum_k 1/(2k)^4=(\pi^4/90)/16$ (hasSum_even); the odd-index subsum is $\sum_k 1/(2k+1)^4=(\pi^4/90)\cdot(15/16)$ (hasSum_odd), obtained by subtracting the even part from the full sum and using uniqueness of unconditional sums in $\mathbb{R}$. Sign lemmas eta_term_even and eta_term_odd identify the alternating terms with $-1/(2k)^4$ and $+1/(2k+1)^4$ respectively.
proof idea
Build two auxiliary HasSums. For even indices, rewrite the alternating term via eta_term_even as $-1/(2k)^4$, then apply hasSum_even.neg to get sum $-(\pi^4/90)/16$. For odd indices, rewrite via eta_term_odd as $+1/(2k+1)^4$ and apply hasSum_odd to get sum $(\pi^4/90)\cdot(15/16)$.
Recombine with Mathlib's HasSum.even_add_odd on the full alternating family. A final convert ... using 1; ring checks that the even-plus-odd total equals $(7/8)\cdot(\pi^4/90)$.
why it matters
This is the series-layer theorem that removes "η(4)/ζ(4)=7/8 is classical" from the MODEL-input list of EntropyPerPhoton. Downstream, eta4_div_zeta4 quotes the two tsums to obtain the bare ratio 7/8, and fermionWeight_eq_eta_zeta_ratio identifies the rational MODEL constant with that ratio: fermionWeight · ζ(4) = η(4).
The integral layer in FermionWeightIntegral reindexes the same identity (hasSum_eta_shift, hasSum_zeta_shift) so the Fermi–Dirac thermodynamic integral can cite an unconditional HasSum rather than an external eta value. Within Recognition Science cosmology this closes the mathematical half of the fermion entropy weight; only the statistical-mechanics identification of the fermionic integral remains as physics input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.