Pith. sign in
module module high

IndisputableMonolith.Cosmology.FermionWeight

show as:
view Lean formalization →

Derives the classical series identity η(4)=(7/8)ζ(4) by splitting the alternating 4-series into even and odd terms. Cosmology and baryogenesis bookkeeping cite it as the pure-series source of the fermion weight 7/8. The argument is elementary p-series summability plus the scaling 1/(2k)^4=(1/16)k^{-4}.

claimThe Dirichlet eta value at four equals seven-eighths of Riemann zeta at four: $\eta(4)=\frac{7}{8}\zeta(4)$, where $\eta(4)=\sum_{n\ge 1}(-1)^{n-1}n^{-4}$ and $\zeta(4)=\sum_{n\ge 1}n^{-4}$.

background

In the cosmology lane, entropy-per-photon bookkeeping mixes Bose and Fermi statistics for Standard Model degrees of freedom. Upstream EntropyPerPhoton builds the numerical ratio from ζ(3), π⁴, and the effective count g*s=43/11 under those statistics.

Fermions enter with an alternating Matsubara sign, so their frequency sum is the Dirichlet eta series η(s)=∑(-1)^{n-1}n^{-s} rather than ζ(s). At s=4 the classical identity η(4)=(7/8)ζ(4) supplies the textbook weight 7/8 that later appears in thermodynamic integrals.

This module isolates that pure series fact (even/odd splitting, summability, ratio) before any integral-layer claim.

proof idea

Even terms are rewritten by the pointwise identity 1/(2k)^4=(1/k^4)/16 (both sides 0 at k=0). Separate HasSum/summable lemmas handle the even and odd p-series pieces; eta is reassembled as their signed combination. Dividing the resulting eta(4) sum by ζ(4) yields the constant 7/8, packaged as the ratio theorem fermionWeight_eq_eta_zeta_ratio.

why it matters in Recognition Science

Downstream FermionWeightIntegral imports the module to bridge the series identity to the thermodynamic statement used in entropy bookkeeping: the Fermi–Dirac energy integral equals 7/8 of the Bose–Einstein integral. That factor feeds g*s and the entropy-per-photon figure in the baryogenesis lane. The module is the analytic prerequisite; without η(4)=(7/8)ζ(4) the integral-layer theorem has no series anchor.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)