Cosmology Fermion Weight Has Sum Even

The even-index sum

The Riemann zeta function at 4, written ζ(4), is the infinite sum 1/1⁴ + 1/2⁴ + 1/3⁴ + ... and equals π⁴/90, about 1.0823. A classical question asks how much of this total comes from the even denominators (2, 4, 6, ...) versus the odd ones (1, 3, 5, ...). The even part is 1/2⁴ + 1/4⁴ + 1/6⁴ + ... = ζ(4)/16, because each even denominator 2k contributes 1/(2k)⁴ = (1/16)·(1/k⁴), and summing over k recovers one sixteenth of the full series.

The declaration hasSum_even in the framework's machine-checked library of formal theorems records exactly this identity as a proved statement: the even-indexed subseries sums to π⁴/(90·16). The proof is a direct manipulation: rewrite each term using the pointwise identity above, then invoke the known result that the full series sums to π⁴/90. No approximation, no physics, and no extra assumptions enter; the statement is purely about real numbers and infinite sums.

This even-part lemma is one step in a larger derivation about the early universe. In the standard cosmological picture, the entropy density just after the big bang receives separate contributions from photons (bosons) and from particles like electrons and neutrinos (fermions). The two species weight their integrals differently: the Fermi–Dirac integral for fermions carries an alternating sign pattern, while the Bose–Einstein integral for photons does not. The framework's library proves that the alternating series η(4) = 1 − 1/2⁴ + 1/3⁴ − 1/4⁴ + ... equals (7/8)·ζ(4), and the even-part lemma is the load-bearing first half of that proof: split ζ(4) into even and odd parts, subtract the even part from the full sum to get the odd part, then combine with signs.

In Recognition Science, this series identity upgrades a numerical input to the cosmological entropy calculation. The factor 7/8 that multiplies the photon entropy when counting fermions was previously taken as a given constant; the library now derives it from the eta/zeta ratio as a theorem. What remains a modeling choice is not the mathematics but the physics: identifying a fermion species with the Fermi–Dirac integral at all. The lemma itself claims nothing about fermions, entropy, or cosmology; it is a statement about integers, powers, and sums, and it is true in any framework that accepts the standard definition of ζ(4).

/-- The even-index part of `ζ(4)`: `∑_k 1/(2k)⁴ = (π⁴/90)/16`. -/
lemma hasSum_even :
    HasSum (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4) (π ^ 4 / 90 / 16) := by
  rw [even_term_eq]
  exact hasSum_zeta_four.div_const 16

/-- **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]

What this page does not claim

The lemma does not claim anything about fermions, entropy, or cosmology; it is a statement about real-number sums. The derivation does not remove the physics input that a fermion species contributes the Fermi–Dirac integral. The result does not depend on any Recognition Science axiom; it holds in standard mathematics.

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: