eta_term_odd
plain-language theorem explainer
For each natural k, the odd-index term of the Dirichlet eta series at s=4 equals the corresponding positive zeta term: (-1)^{2k+2}/(2k+1)^4 = 1/(2k+1)^4. Anyone building η(4) by even/odd recombination of ζ(4) cites this sign identity. The proof is a one-line Even witness plus Mathlib's neg_one_pow rewrite.
Claim. For every natural number $k$, $(-1)^{2k+2}/(2k+1)^4 = 1/(2k+1)^4$ as real numbers.
background
The module upgrades the cosmology MODEL input fermionWeight = 7/8 to a derived series identity η(4) = (7/8)·ζ(4). Here ζ(4) = ∑ 1/n⁴ = π⁴/90 and η(4) = ∑ (-1)^{n+1}/n⁴ is the Dirichlet eta value that enters the Fermi–Dirac integral ∫ x³/(eˣ+1) dx = Γ(4)·η(4), while the Bose–Einstein side uses ζ(4).
The derivation splits ζ(4) into even-index and odd-index parts, then writes the alternating series as odd-part minus even-part. This lemma is the odd-index sign step: at n = 2k+1 the alternating factor is (-1)^{2k+2}, which is +1, so those terms coincide with the odd zeta terms. An identical lemma for power 3 lives in NumberDensityIntegral.
proof idea
Term-mode proof in two steps. First construct an Even witness for the exponent 2k+1+1 by exhibiting the half-integer k+1 (via ring). Then rewrite with Mathlib's Even.neg_one_pow, which replaces (-1) raised to an even power by +1, leaving the positive reciprocal fourth power on the right-hand side.
why it matters
Feeds hasSum_eta_four, the unconditional HasSum statement that ∑ (-1)^{n+1}/n⁴ = (7/8)·(π⁴/90), i.e. η(4) = (7/8)·ζ(4). That theorem, together with the even-term companion and the even/odd recombination, yields fermionWeight_eq_eta_zeta_ratio, which removes the classical eta/zeta identity from the MODEL-input list of EntropyPerPhoton and leaves only the statistical-mechanics claim that a fermion species contributes the Fermi–Dirac integral. The same pattern is reused for η(3) in NumberDensityIntegral. Within RS cosmology this is pure classical analysis scaffolding the 7/8 fermion entropy weight; it does not touch the forcing chain T0–T8 or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.