Cosmology Fermion Weight Summable Odd

The odd-index tail

The Dirichlet eta function at 4, written η(4), is the infinite sum 1 − 1/2⁴ + 1/3⁴ − 1/4⁴ + …, and it equals 7/8 times ζ(4), where ζ(4) = 1 + 1/2⁴ + 1/3⁴ + … = π⁴/90. That identity is classical, known since the 18th century. The proof splits ζ(4) into its even-index terms (n = 2, 4, 6, …) and odd-index terms (n = 1, 3, 5, …). The even part is 1/16 of the whole; the odd part is the remaining 15/16. The alternating series η(4) then equals the odd part minus the even part, giving (15/16 − 1/16)ζ(4) = 14/16 ζ(4) = 7/8 ζ(4).

The declaration summable_odd is the step that makes this split rigorous: it proves that the odd-index series ∑ 1/(2k+1)⁴ converges. Convergence is what allows the even and odd parts to be recombined without ambiguity. Without it, the subtraction step would be informal. The proof is short: the full series ∑ 1/n⁴ converges (it is ζ(4)), and the map k ↦ 2k+1 is injective, so the odd-index subsequence converges to the same kind of limit. This is a theorem in the framework's machine-checked library of formal theorems, with no extra axioms beyond the standard logical ones.

What summable_odd does not claim is the value of the odd sum, nor the 7/8 factor itself. Those come from later lemmas in the same file. It also does not claim that the odd series converges to 15/16 of ζ(4); that value is derived separately by subtraction. And it says nothing about physics: the factor 7/8 appears in cosmology as the fermion entropy weight, but summable_odd is purely a statement about real series. The physical identification, that a fermion species contributes the Fermi–Dirac integral, remains a modeling choice, not a theorem.

In the framework's cosmology account, the 7/8 factor is the ratio η(4)/ζ(4), and summable_odd is the load-bearing convergence fact that lets the series identity be proved rather than assumed. For a reader, the practical consequence is that the split of ζ(4) into even and odd parts is not a hand-wave: it is a checked step in a chain that upgrades a numerical input into a derived identity.

lemma summable_odd :
    Summable (fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4) := by
  have h : Summable (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) := hasSum_zeta_four.summable
  have hinj : Function.Injective (fun k : ℕ => 2 * k + 1) := by
    intro a b hab
    simp only at hab
    omega
  have h2 := h.comp_injective hinj
  exact h2.congr fun k => by simp only [Function.comp_apply]

/-- **THEOREM (η(4) as a `HasSum`).** The alternating series
`∑ (−1)^(n+1)/n⁴` converges unconditionally to `(7/8)·(π⁴/90)`,
i.e. `η(4) = (7/8)·ζ(4)`. -/
theorem hasSum_eta_four :
    HasSum (fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4)
      (7 / 8 * (π ^ 4 / 90)) := by
  have he : HasSum
      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 4)
      (-(π ^ 4 / 90 / 16)) := by
    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1) / ((2 * k : ℕ) : ℝ) ^ 4)
        = fun k : ℕ => -((1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4) := by
      funext k; exact eta_term_even k
    rw [hfun]
    exact hasSum_even.neg
  have ho : HasSum
      (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 4)
      (π ^ 4 / 90 * (15 / 16)) := by
    have hfun : (fun k : ℕ => (-1 : ℝ) ^ (2 * k + 1 + 1) / ((2 * k + 1 : ℕ) : ℝ) ^ 4)
        = fun k : ℕ => (1 : ℝ) / ((2 * k + 1 : ℕ) : ℝ) ^ 4 := by
      funext k; exact eta_term_odd k
    rw [hfun]
    exact hasSum_odd
  have h := HasSum.even_add_odd
    (f := fun n : ℕ => (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4) he ho
  convert h using 1
  ring

/-- **THEOREM (the eta/zeta ratio).** `η(4) / ζ(4) = 7/8` as real numbers. -/
theorem eta4_div_zeta4 :
    (∑' n : ℕ, (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4)
      / (∑' n : ℕ, (1 : ℝ) / (n : ℝ) ^ 4) = 7 / 8 := by
  rw [hasSum_eta_four.tsum_eq, hasSum_zeta_four.tsum_eq]
  have hz : (π : ℝ) ^ 4 / 90 ≠ 0 := by positivity
  rw [mul_div_assoc, div_self hz, mul_one]

/-- **THEOREM (fermion weight provenance).** The `7/8` MODEL constant in
`EntropyPerPhoton.fermionWeight` is exactly the eta/zeta ratio:
`fermionWeight · ζ(4) = η(4)`. The series identity is now derived, not
imported; the remaining MODEL content of the weight is only the
statistical-mechanics identification of the fermionic entropy integral. -/
theorem fermionWeight_eq_eta_zeta_ratio :
    ((EntropyPerPhoton.fermionWeight : ℚ) : ℝ)
        * ∑' n : ℕ, (1 : ℝ) / (n : ℝ) ^ 4
      = ∑' n : ℕ, (-1 : ℝ) ^ (n + 1) / (n : ℝ) ^ 4 := by
  rw [hasSum_eta_four.tsum_eq, hasSum_zeta_four.tsum_eq]
  unfold EntropyPerPhoton.fermionWeight
  push_cast
  ring

What this page does not claim

summable_odd does not claim the value of the odd series, only its convergence. The statistical mechanics identification of the fermion entropy integral is a modeling choice, not a theorem. The declaration does not claim any physical content about fermions or cosmology.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/FermionWeight.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: