bosePartition
plain-language theorem explainer
The bosonic single-mode grand partition function at dimensionless energy $t=E/T$ is the sum of Gibbs weights $e^{-nt}$ over all natural-number occupancies. Statistical-mechanics and cosmology results in the η_B chain cite it as the primitive from which Bose pressure and energy kernels are derived rather than postulated. The declaration is a direct definition: a tsum of Boltzmann weights at chemical potential zero.
Claim. For $t \in \mathbb{R}$, the bosonic single-mode grand partition function is $Z_B(t) = \sum_{n=0}^{\infty} e^{-n t}$, summing Gibbs weights over unrestricted occupancy $n \in \mathbb{N}$ at chemical potential zero.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure kernels $\mp\ln(1\mp e^{-t})$ and energy kernels $t/(e^t\mp 1)$ from the single-mode grand partition function at $\mu=0$, with $t=E/T$ dimensionless. Earlier modules (PhaseSpaceReduction, GrandPotential) took those kernels as model inputs; here the only inputs are the Gibbs weight and the occupancy sets ($n\in\mathbb{N}$ for bosons, $n\in{0,1}$ for fermions).
The Gibbs weight of the $n$-quanta microstate is $w_n=e^{-n t}$. The bosonic partition is the unrestricted sum of those weights. Downstream, the geometric series identity yields $Z_B=(1-e^{-t})^{-1}$ for $t>0$, and $\ln Z_B$ recovers the pressure kernel that had been defined by hand.
proof idea
Pure definition: $Z_B(t)$ is introduced as the tsum $\sum'_n w_n(t)$ with $w_n(t)=e^{-n t}$. No proof obligations; noncomputable because of the infinite sum over $\mathbb{N}$.
why it matters
This is the bosonic starting object of the module's derivation chain. It feeds bosePartition_eq (geometric series closed form), positivity, the mean occupation $\langle n\rangle=(\sum n w_n)/Z_B$, and the identification of the Bose pressure kernel with $\ln Z_B$. Thermodynamic consistency theorems then show $\langle n\rangle=-d(\ln Z)/dt$ and, in physical variables, $\langle E\rangle=-\partial_\beta\ln Z$ per mode.
The capstone plasmaPressure_from_partitionFunction rewrites plasma pressure in the η_B chain as a phase-space integral of $T\cdot\ln Z_{\mathrm{mode}}(E/T)$, so the log kernels cease to be independent inputs. Only Gibbs weights and occupancy sets remain. That closes the provenance gap between postulated Bose kernels and grand-canonical statistical mechanics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.