Pith. sign in
module module high

IndisputableMonolith.Cosmology.NumberDensityIntegral

show as:
view Lean formalization →

Establishes the number-density integral identities behind the cosmological entropy chain: the shifted cubic sum equals ζ(3), plus the Bose Mellin transform at order 3 and the even/odd η(3) decompositions. Anyone deriving entropy-per-photon or radiation entropy from Fermi–Dirac and Bose–Einstein statistics would cite it. Proofs split even and odd series, match termwise identities, and discharge summability via Mathlib power-sum lemmas.

claimThe module proves $\sum_{n\ge 0}(n+1)^{-3}=\zeta(3)$ as the defining sum of the entropy-per-photon constant, the Bose number-density Mellin identity at cubic order, and the even/odd decompositions of the alternating cubic series $\eta(3)$ used for fermionic weights.

background

In the Recognition Science cosmology lane, entropy bookkeeping for a massless quantum gas needs concrete values of the Bose and Fermi number-density integrals. Those integrals reduce to Dirichlet series: the Riemann zeta value $\zeta(3)=\sum_{n\ge 1}n^{-3}$ for bosons, and the alternating eta value $\eta(3)$ for fermions.

The sibling module EntropyPerPhoton takes $\zeta(3)$, $\pi^4$, and the Standard Model effective count $g_{*s}=43/11$ as inputs to the entropy-per-photon ratio used by baryogenesis. FermionWeightIntegral already closed the energy-integral gap $\eta(4)=(7/8)\zeta(4)$; the present module supplies the parallel cubic (number-density) layer.

Notation follows Mathlib: HasSum statements for unshifted and shifted power sums, even/odd term extractions, and the Mellin-type Bose sum at exponent 3.

proof idea

The module is a cluster of analysis lemmas, not a single theorem. Unshifted and shifted cubic zeta sums are identified by reindexing. Even and odd subsum series are extracted termwise; each is shown summable, then reassembled into $\zeta(3)$ and $\eta(3)$ HasSum statements. Parallel lemmas treat the alternating eta terms and the Bose Mellin transform at cubic order. All steps are classical real-series arguments over Mathlib summability infrastructure; no physical hypotheses enter.

why it matters in Recognition Science

RadiationEntropyRelation imports this module and records that the entropy chain (EntropyPerPhoton together with NumberDensityIntegral) previously treated the thermodynamic factor $4/3$ as an input; that parent module then derives $s=(4/3)\rho/T$ from the entropy functional. Without the cubic number-density identities here, the $\zeta(3)$ constant inside the entropy-per-photon ratio has no analytic anchor. The module therefore sits between the pure series layer and the MODEL entropy bookkeeping that feeds the $\eta_B$ baryogenesis lane. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; its role is the classical-analysis substrate of the cosmology entropy stack.

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)