hasSum_even
plain-language theorem explainer
The even-index subsum of ζ(4) equals (π⁴/90)/16: ∑_k 1/(2k)⁴ = ζ(4)/16. Cosmology and statistical-mechanics arguments that derive η(4)=(7/8)ζ(4) for the Fermi–Dirac entropy weight cite this as the even half of the split. The proof is a two-line rewrite: apply the pointwise identity 1/(2k)⁴=(1/k⁴)/16, then scale Mathlib's unconditional sum for ζ(4) by the constant 16.
Claim. The series $\sum_{k=0}^{\infty} 1/(2k)^4$ converges unconditionally over $\mathbb{N}$ to $(\pi^4/90)/16$. (The $k=0$ term is zero by the usual convention $1/0^4=0$ in this formal sum.)
background
The module upgrades the MODEL input fermionWeight = 7/8 used in photon-entropy bookkeeping to a derived series identity η(4)=(7/8)·ζ(4). Here ζ(4)=∑ 1/n⁴ = π⁴/90 is Mathlib's classical Basel-type sum, and η(4)=∑ (−1)^{n+1}/n⁴ is the Dirichlet eta value that appears in the Fermi–Dirac integral ∫ x³/(eˣ+1) dx = Γ(4)·η(4).
The derivation splits ζ(4) into even and odd indices. The even part is the present sum: re-index n=2k to get ∑ 1/(2k)⁴ = (1/16)·ζ(4). The companion odd sum is then full-minus-even, and the alternating series is odd-minus-even, yielding the factor 7/8.
Upstream, the pointwise lemma even_term_eq records 1/(2k)⁴ = (1/k⁴)/16 for every k (both sides zero at k=0). The same pattern appears for the cubic case in NumberDensityIntegral, with divisor 8 instead of 16.
proof idea
One-line algebraic reduction after a rewrite. First rewrite the summand family by even_term_eq, which equates fun k ↦ 1/(2k)⁴ with fun k ↦ (1/k⁴)/16 pointwise (including the vanishing k=0 term). The goal becomes HasSum (fun k ↦ (1/k⁴)/16) (π⁴/90 / 16). Apply HasSum.div_const to Mathlib's hasSum_zeta_four, which supplies HasSum (fun n ↦ 1/n⁴) (π⁴/90), scaling the sum by the constant 16.
why it matters
This is the even half of the classical even/odd split that produces η(4)=(7/8)ζ(4). Downstream, hasSum_odd obtains the odd subsum (π⁴/90)·(15/16) by subtracting the present sum from the full ζ(4) sum via HasSum.even_add_odd and uniqueness of unconditional sums in ℝ. That odd sum, together with the even sum, feeds hasSum_eta_four, which states the alternating series converges to (7/8)·(π⁴/90).
The terminal theorem fermionWeight_eq_eta_zeta_ratio then identifies the rational 7/8 used in EntropyPerPhoton.fermionWeight with the pure series ratio η(4)/ζ(4). The module doc is explicit: this removes "the eta/zeta series identity is classical" from the MODEL-input list, leaving only the statistical-mechanics claim that a fermion species contributes the Fermi–Dirac integral. The cubic analogue in NumberDensityIntegral follows the same even-sum pattern for η(3)=(3/4)ζ(3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.