module module moderate

`IndisputableMonolith.Cosmology.StatisticsKernels`

Defines the elementary statistical kernels used in RS cosmology: Gibbs weights, Bose and Fermi partition functions, and occupation numbers at chemical potential zero. Cosmologists citing the reduced pressure and energy integrals need these closed forms. The module is mostly definitional, with short positivity and algebraic identities proved from Real.exp facts.

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 single-mode partitions are $Z_B(t) = \sum_{n=0}^{\infty} e^{-n t} = (1-e^{-t})^{-1}$ and $Z_F(t) = 1+e^{-t}$, with occupations $n_B = (e^{t}-1)^{-1}$ and $n_F = (e^{t}+1)^{-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 kernel $K$ is built from Bose or Fermi statistics at vanishing chemical potential.

This module supplies those kernels in dimensionless variables. The Gibbs weight of an $n$-quanta microstate at $t=E/T$ is $e^{-n t}$. Summing geometric series yields the Bose partition $(1-e^{-t})^{-1}$ and the two-level Fermi partition $1+e^{-t}$. Occupation numbers are the usual logarithmic derivatives.

Upstream, PhaseSpaceReduction records that the prefactor $g/(2\pi^2)$ is forced by three spatial dimensions; the present kernels are the statistical content that multiplies that geometric factor.

proof idea

Definition module with lightweight supporting lemmas. Boltzmann weights, partitions, and occupations are introduced as plain defs in terms of Real.exp. Identities such as $w_n = (e^{-t})^n$, $Z_B = (1-e^{-t})^{-1}$, and $Z_F = 1+e^{-t}$ are one-line algebraic rewrites. Positivity of the partitions follows from $e^{-t}<1$ (for $t>0$) and $e^{t}>1$. No deep analysis; Mathlib exponential inequalities close the goals.

why it matters in Recognition Science

Feeds the integrand kernels inside the RS plasma pressure and energy functionals that PhaseSpaceReduction writes as $P=(g/2\pi^2)T^4\int t^2 K(t),dt$. Without explicit Bose/Fermi partitions and occupations, those integrals remain formal. The module sits in the cosmology layer that converts the forced $D=3$ phase-space measure into thermodynamic observables, consistent with the eight-tick and dimension-forcing chain (T7–T8) that fixes the geometric prefactor. No downstream theorems are wired yet in the graph; the natural consumers are the grand-potential pressure and energy theorems.

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 interacting gases.
Does not evaluate the momentum integrals; only supplies the statistical kernels $K(t)$.
Does not claim RS-specific corrections beyond standard Bose/Fermi forms at $\mu=0$.

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