Cosmology Fermion Weight Even Term Eq

The even-term identity

The number π⁴/90 is the sum of the reciprocals of the fourth powers of all positive integers: 1 + 1/16 + 1/81 + 1/256 + ... This sum, written ζ(4), was evaluated by Leonhard Euler in 1735, and it appears throughout physics wherever radiation or heat is counted. The declaration even_term_eq concerns a simple but useful fact about this sum: if you take only the even terms, 1/16 + 1/256 + ..., you get exactly one sixteenth of the whole sum. That is, the even-indexed part of ζ(4) equals ζ(4)/16.

The proof is a re-indexing. Each even term 1/(2k)⁴ equals (1/k⁴)/16, so summing over k from 0 upward just pulls the factor 1/16 out of the whole series. The declaration states this pointwise identity for every natural number k, including k = 0 where both sides are zero. It is a lemma in the framework's machine-checked library of formal theorems, and it is used as the first step in splitting ζ(4) into its even and odd parts, a split that later yields the alternating series value η(4) = (7/8)ζ(4).

In Recognition Science, this identity feeds a larger result about the entropy of the early universe. The framework models a fermion species as contributing a factor of 7/8 relative to a boson species in the entropy per photon, a standard statistical-mechanics ratio. The theorem fermionWeight_eq_eta_zeta_ratio shows that this 7/8 is exactly the ratio η(4)/ζ(4), so the series identity is now derived inside the library rather than assumed. The even_term_eq lemma is the first concrete step of that derivation.

The declaration does not claim anything about the physics of fermions. It only establishes a fact about infinite series: the even-indexed terms of the fourth-power sum are one sixteenth of the total. The statistical-mechanics statement that a fermion species contributes the Fermi-Dirac integral, and hence the 7/8 weight, remains a modeling choice in the framework, not a theorem. The mathematics is proved; the physics input is identified and left as a definition.

/-- Pointwise identity `1/(2k)⁴ = (1/k⁴)/16`, including `k = 0` where both
sides are `0` (division by zero). -/
lemma even_term_eq :
    (fun k : ℕ => (1 : ℝ) / ((2 * k : ℕ) : ℝ) ^ 4)
      = fun k : ℕ => ((1 : ℝ) / (k : ℝ) ^ 4) / 16 := by
  funext k
  rcases Nat.eq_zero_or_pos k with hk | hk
  · subst hk; norm_num
  · have hk' : (k : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hk.ne'
    push_cast
    field_simp
    ring

/-- **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 declaration does not prove any physical statement about fermions or entropy. The statistical-mechanics identification of the 7/8 weight remains a modeling choice, not a theorem.

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: