module module moderate

`IndisputableMonolith.Cosmology.StatisticsKernels`

Defines the elementary statistical-mechanics kernels used in RS cosmology: Gibbs weights e^{-n t}, Bose and Fermi single-mode partition functions, and the corresponding occupation numbers at chemical potential zero. Cosmology and thermal-history calculations cite these as the integrands feeding phase-space reduced pressure and energy. The module is mostly definitional, with short positivity and closed-form identities proved from Mathlib exponentials.

claimFor dimensionless energy $t = E/T$ and occupation number $n \in \mathbb{N}$, the Gibbs weight is $w_n(t) = e^{-n t}$. The Bose and Fermi partition functions are $Z_B(t) = \sum_{n=0}^{\infty} e^{-n t} = 1/(1-e^{-t})$ (for $t>0$) and $Z_F(t) = \sum_{n=0}^{1} e^{-n t} = 1+e^{-t}$. Occupation numbers are $n_B(t) = 1/(e^{t}-1)$ and $n_F(t) = 1/(e^{t}+1)$.

background

Recognition Science cosmology reduces the relativistic ideal-gas pressure and energy in $D=3$ to one-dimensional integrals of the form $(g/2\pi^2) T^4 \int t^2 K(t),dt$. The upstream PhaseSpaceReduction module records that prefactor and the reduced shapes of plasma pressure and energy; the kernels $K(t)$ themselves are built from Bose or Fermi statistics at vanishing chemical potential.

This module supplies those kernels in dimensionless variables $t=E/T$ (equivalently $\beta E$). The Gibbs weight of an $n$-quanta microstate is $w_n=e^{-n t}$. Summing over $n$ yields the single-mode Bose and Fermi partition functions; logarithmic derivatives (or direct series) give the mean occupation numbers. All quantities are stated for $\mu=0$, the regime used in the standard early-universe plasma integrals.

proof idea

Primarily a definition module. Boltzmann weights, partitions, and occupations are introduced as defs. Short lemmas then record: power laws for iterated weights; elementary inequalities $e^{-t}<1$ and $1<e^{t}$ for $t>0$; closed forms $Z_B=1/(1-e^{-t})$ and $Z_F=1+e^{-t}$; and strict positivity of both partitions. Proofs are direct Mathlib exponential algebra and geometric-series summation, with no deep RS-specific forcing.

why it matters in Recognition Science

Feeds the phase-space reduced plasma pressure and energy constructed in Cosmology.PhaseSpaceReduction, which quote the $g/(2\pi^2)\cdot T^4$ prefactor forced by $D=3$ (forcing landmark T8). Without explicit Bose/Fermi kernels the reduced integrals remain schematic. Downstream cosmology (equation of state, $g_*$, entropy density) depends on these occupation factors remaining the standard $\mu=0$ expressions. The module does not itself close any forcing-chain step; it is infrastructure so that thermal integrals sit on named, positivity-checked objects rather than ad-hoc formulas.

scope and limits

Does not derive the $g/(2\pi^2)T^4$ prefactor; that lives in PhaseSpaceReduction.
Does not treat nonzero chemical potential or conserved charges.
Does not evaluate momentum integrals or compute $g_*$, pressure, or energy densities.
Does not address interacting plasmas, mass thresholds, or nonequilibrium distributions.
Does not connect occupation numbers to RS mass-ladder or phi-rung formulas.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.PhaseSpaceReduction module_import

declarations in this module (31)

def boltzmannWeight L71
def bosePartition L75
def fermiPartition L79
def boseOccupation L83
def fermiOccupation L87
lemma boltzmannWeight_pow L91
lemma exp_neg_lt_one L97
lemma one_lt_exp L100
theorem bosePartition_eq L108
theorem fermiPartition_eq L117
lemma bosePartition_pos L122
lemma fermiPartition_pos L127
theorem boseLogKernel_eq_log_partition L136
theorem fermiLogKernel_eq_log_partition L143
theorem boseOccupation_eq L153
theorem fermiOccupation_eq L173
theorem fermiOccupation_lt_one L189
theorem boseOccupation_pos L196
theorem boseEnergyKernel_eq_occupation L205
theorem fermiEnergyKernel_eq_occupation L212
theorem boseLogKernel_hasDerivAt L224
theorem fermiLogKernel_hasDerivAt L249
theorem boseEnergyKernel_from_logKernel L272
theorem fermiEnergyKernel_from_logKernel L278
theorem mode_energy_bose L288
theorem mode_energy_fermi L304
lemma phaseSpaceDensity_congr_pos L322
theorem plasmaPressure_from_partitionFunction L339
theorem plasmaEnergy_from_occupation L356
theorem number_integrand_bose L374
theorem number_integrand_fermi L380