Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.NumberDensityIntegral

show as:
view Lean formalization →

Number-density integrals for massless Bose and Fermi gases reduce to the cubic zeta and eta series. The module proves HasSum identities identifying the shifted sum ∑(n+1)^{-3} with ζ(3), plus even/odd and Mellin forms used in entropy bookkeeping. Anyone citing the entropy-per-photon ratio or the radiation entropy relation needs these analytic closures. Arguments are classical summability and term-splitting over Mathlib series infrastructure.

claimThe module establishes $\sum_{n\geq 0}(n+1)^{-3}=\zeta(3)$ as a HasSum identity, the even/odd decompositions of that series, the Dirichlet eta form $\eta(3)=\sum_{n\geq 0}(-1)^n(n+1)^{-3}$, and the Mellin-type Bose number-density integral at cubic weight.

background

In the Recognition Science cosmology lane, the entropy-per-photon ratio is assembled from $\zeta(3)$, $\pi^4$, and the effective relativistic degrees of freedom $g_{*s}=43/11$. The upstream EntropyPerPhoton module treats $\zeta(3)$ as a named constant whose series definition must be discharged analytically before the arithmetic ratio is trusted.

Number density for a massless Bose gas is proportional to an integral that Mellin-transforms into $\sum n^{-3}=\zeta(3)$. The Fermi case uses the alternating eta series. FermionWeightIntegral already closed the energy-integral $7/8$ factor at the thermodynamic layer; this module supplies the companion number-density summability facts.

The local setting is classical real analysis: absolute summability of $p$-series at $p=3$, shift equivalences, and even/odd splitting that relates $\zeta$ to $\eta$.

proof idea

A cluster of HasSum lemmas, not a single theorem. Unshifted and shifted cubic $p$-series are identified with $\zeta(3)$ by reindexing. Even and odd subsumes are split out; the odd part yields the $\eta(3)$ alternating sum after sign bookkeeping. Summability of the shifted $r\mapsto r^{-3}$ series is recorded so the Mellin–Bose identity at weight 3 can invoke HasSum rather than bare Summable. All steps are Mathlib-style termwise algebra plus standard $p$-series tests; no Recognition-specific axioms enter.

why it matters in Recognition Science

RadiationEntropyRelation imports this module and records that the entropy chain (EntropyPerPhoton together with NumberDensityIntegral) previously used the $4/3$ thermodynamic factor as an assumed input; that parent theorem derives $s=(4/3)\rho/T$ from the entropy functional for a massless quantum gas.

Without the $\zeta(3)/\eta(3)$ HasSum closures here, the number-density side of the entropy-per-photon ratio remains a floating model constant rather than a proved series identity. In the broader baryon-asymmetry ($\eta_B$) lane these integrals feed the entropy bookkeeping that converts photon-normalized yields into physical densities. The module sits at the analysis layer between FermionWeightIntegral and the radiation entropy relation, closing MODEL inputs rather than RS forcing-chain steps (T0–T8).

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (25)