boseOccupation
plain-language theorem explainer
Defines the ensemble-mean occupation of a single bosonic mode at dimensionless energy t = E/T and μ = 0 as the weighted sum Σ n w_n divided by the bosonic partition function. Cosmology and statistical-mechanics arguments cite it as the primitive ⟨n⟩_B before proving it equals 1/(e^t − 1). The body is a direct quotient of two series built from Gibbs weights.
Claim. For dimensionless energy $t \in \mathbb{R}$, the mean bosonic occupation is $\langle n \rangle_B(t) = \bigl(\sum_{n=0}^{\infty} n\, e^{-n t}\bigr) / Z_B(t)$, where $Z_B(t) = \sum_{n=0}^{\infty} e^{-n t}$ is the single-mode grand partition function at $\mu = 0$.
background
This module rebuilds the Bose/Fermi pressure and energy kernels from the grand partition function of one mode at vanishing chemical potential. The only inputs are the Gibbs weight $w_n = e^{-n t}$ of the $n$-quanta microstate and the occupancy set: unrestricted $n \in \mathbb{N}$ for bosons.
Upstream, boltzmannWeight is exactly that Gibbs factor $w_n = e^{-n t}$. The bosonic partition $Z_B(t) = \sum_n w_n$ is the geometric series over all occupancies. Mean occupation is the standard ensemble average $\langle n \rangle = (\sum n w_n)/Z$, written here before any closed form is proved.
Earlier layers (PhaseSpaceReduction, GrandPotential) treated $t/(e^t-1)$ as a model definition. Here that kernel is derived: occupation first, then energy as $t\cdot\langle n\rangle$.
proof idea
Pure definition, not a theorem. The body is the quotient of two series: numerator $\sum'_{n:\mathbb{N}} n \cdot$ boltzmannWeight $t, n$, denominator bosePartition $t$. No tactics, no lemmas applied at the definition site. Closed-form identification and positivity are deferred to later theorems that unfold this def.
why it matters
This is the primitive Bose occupation that the module's main theorems evaluate and differentiate. Downstream, boseOccupation_eq proves the Bose–Einstein law $\langle n\rangle_B = 1/(e^t-1)$ via the weighted geometric series; boseOccupation_pos gives positivity for $t>0$.
Energy consistency rides on it: boseEnergyKernel_eq_occupation states the plasma energy integrand is $t\cdot\langle n\rangle_B$, and boseLogKernel_hasDerivAt shows $\langle n\rangle_B = -\partial_t\ln Z_B$, so pressure and energy kernels are one thermodynamic input. mode_energy_bose lifts that to physical variables $\langle E\rangle = -\partial_\beta\ln Z_B$. Number-density work uses it in number_integrand_bose ($t^2\langle n\rangle_B = t^2/(e^t-1)$), and the η_B plasma capstone plasmaEnergy_from_occupation starts from this occupation rather than an ad hoc kernel.
In the Recognition cosmology stack this closes the gap between phase-space MODEL kernels and genuine grand-canonical bookkeeping for bosonic modes (photons, etc.).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.