Cosmology Fermion Weight Fermion Weight Eq Eta Zeta Ratio

The 7/8 fermion weight

In the standard picture of the early universe, the entropy carried by each species of particle depends on whether it is a fermion or a boson. A fermion species, such as an electron or neutrino, contributes a factor of 7/8 relative to a boson species at the same temperature. This 7/8 is a familiar constant in cosmology textbooks, where it appears in the effective number of relativistic degrees of freedom that sets the expansion rate and temperature history of the hot early universe.

The factor traces to a pair of integrals over particle momenta. A boson species gives the integral ∫ x³/(eˣ−1) dx, which evaluates to Γ(4)·ζ(4), where ζ(4) = Σ 1/n⁴ = π⁴/90. A fermion species gives ∫ x³/(eˣ+1) dx, which evaluates to Γ(4)·η(4), where η(4) = Σ (−1)^(n+1)/n⁴ is the alternating version of the same series. The ratio of the two integrals is therefore η(4)/ζ(4).

The Recognition Science framework's machine-checked library of formal theorems proves that this ratio is exactly 7/8. The proof splits the boson series into even and odd index terms. The even terms sum to ζ(4)/16, the odd terms to 15ζ(4)/16. The alternating fermion series is the odd part minus the even part, so η(4) = (15/16 − 1/16)·ζ(4) = (14/16)·ζ(4) = (7/8)·ζ(4). The final theorem, fermionWeight_eq_eta_zeta_ratio, states this identity directly: the 7/8 weight times ζ(4) equals η(4).

What the theorem changes is the status of the 7/8 factor. In the framework's cosmology module, the factor was previously an input assumption, a model choice. The series identity upgrades the mathematics: the 7/8 is now derived from the definition of the two series, with no axioms beyond the base three of the ambient type theory. What remains a model choice is the physics, the statistical mechanics statement that a fermion species contributes the Fermi–Dirac integral in the first place.

In Recognition Science, this identity is one small rung in a larger forcing chain that derives physical constants from a single cost function. But the eta/zeta identity itself is classical mathematics, available to any cosmology calculation. The framework's contribution is to make the provenance exact: the 7/8 is not an empirical fit and not a free parameter, but a proved consequence of how the two series are defined.

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

The theorem does not derive the statistical mechanics statement that a fermion species contributes the Fermi–Dirac integral. The theorem does not fit the 7/8 factor to any cosmological observation. The identity does not depend on the Recognition Science cost function or forcing chain; it is classical series 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: