IndisputableMonolith.Cosmology.FermionWeight
Establishes the classical series identity η(4)=(7/8)ζ(4), the fermion statistical weight in cosmological entropy bookkeeping. Cosmologists and RS baryogenesis lanes cite it when converting Bose sums to Fermi–Dirac ones. The argument splits the alternating eta series into even and odd parts, uses the pointwise scaling 1/(2k)^4=(1/16)k^{-4}, and compares HasSum statements to extract the 7/8 factor.
claimThe Dirichlet eta value at four equals seven-eighths of Riemann zeta: $\eta(4)=\frac{7}{8}\zeta(4)$, as the ratio of the absolutely convergent series $\sum_{n\ge 1}(-1)^{n-1}n^{-4}$ and $\sum_{n\ge 1}n^{-4}$. Supporting lemmas give the even-term identity $(2k)^{-4}=16^{-1}k^{-4}$ (including the $k=0$ convention $0=0$) and the corresponding HasSum decompositions.
background
In thermal cosmology the entropy and energy densities of relativistic species differ by statistics: Bose–Einstein integrals are controlled by $\zeta(s)$, while Fermi–Dirac integrals bring in the alternating Dirichlet eta $\eta(s)=\sum_{n\ge 1}(-1)^{n-1}n^{-s}$. At $s=4$ the classical identity $\eta(4)=(7/8)\zeta(4)$ supplies the familiar $7/8$ fermion weight used in $g_{*s}$ bookkeeping.
The parent EntropyPerPhoton module already derives the entropy-per-photon ratio from $\zeta(3)$, $\pi^4$, and the Standard Model value $g_{*s}=43/11$ for the baryogenesis lane. This module isolates the pure series fact $\eta(4)/\zeta(4)=7/8$ that underwrites the fermionic half of that arithmetic, without yet passing to continuum energy integrals.
Notation is standard: $\zeta(4)=\pi^4/90$, and $\eta$ is the alternating counterpart. All sums are treated via Mathlib HasSum/Summable so the even/odd split is rigorous at the level of unconditional convergence.
proof idea
The module is a short analysis chain, not a single wrapper. First a pointwise identity equates $(2k)^{-4}$ with $16^{-1}k^{-4}$ (both sides zero at $k=0$). Even and odd subseries of $\eta$ are identified: even terms rescale to a multiple of the full $\zeta$ series, odd terms remain alternating. Summability and HasSum lemmas assemble $\eta(4)$ from those pieces, then the ratio $\eta(4)/\zeta(4)$ simplifies algebraically to $7/8$. The final named theorem packages that ratio as the fermion weight.
why it matters in Recognition Science
Downstream, FermionWeightIntegral imports this module to close the gap from the series identity to the thermodynamic statement actually used in entropy bookkeeping: the Fermi–Dirac energy integral equals $7/8$ of the Bose–Einstein integral. Without $\eta(4)=(7/8)\zeta(4)$ that integral-layer theorem has nothing to quote.
In the broader RS cosmology lane the $7/8$ weight feeds $g_{*s}$ and the entropy-per-photon ratio (EntropyPerPhoton), which in turn enter baryogenesis and relic-density arithmetic. The module therefore sits between pure special-function identities and the model-level particle-content inputs of the Standard Model thermal history. It does not itself invoke Recognition-specific constants ($\phi$, eight-tick structure); it is the classical analytic prerequisite those later steps rely on.
scope and limits
- Does not prove the continuum Fermi–Dirac vs Bose–Einstein integral identity (that is FermionWeightIntegral).
- Does not derive $g_{*s}=43/11$ or the entropy-per-photon numerical value.
- Does not treat $\eta(s)/\zeta(s)$ at $s\neq 4$ or conditional convergence issues for $s\le 1$.
- Does not introduce RS-native constants ($\phi$, rung masses, or eight-tick structure).
- Does not address interacting or massive species beyond free relativistic statistics.