bose_occupation
plain-language theorem explainer
The mean occupancy of a bosonic mode equals the Bose–Einstein distribution 1/(e^t − 1). Cosmology and thermal-history proofs cite it to replace the ratio of weighted geometric series by the closed form. The proof substitutes the closed forms of the occupancy-weighted sum and the partition tsum, then clears denominators with the identity e^{−t} e^t = 1.
Claim. For every real $t > 0$, $$\frac{\sum_{n=0}^{\infty} n\, e^{-nt}}{\sum_{n=0}^{\infty} e^{-nt}} = \frac{1}{e^{t}-1}.$$
background
This module builds the statistical-mechanics floor under the cosmology thermal-history chain: per-mode grand partition functions, the log kernels consumed by phase-space reduction, and the mean occupation numbers. Everything is written with $x = e^{-t}$ and $t > 0$, so $0 < x < 1$ and every series converges.
For bosons the occupancy runs over all of $\mathbb{N}$. The partition function is the geometric series $Z_B = \sum x^n = (1-x)^{-1}$, already recorded as bose_partition_tsum. The occupancy-weighted companion $\sum n, x^n = x/(1-x)^2$ is bose_weighted_hasSum. The mean occupancy is their ratio $\langle n\rangle = (\sum n, x^n)/(\sum x^n)$.
The only physical fork between Bose and Fermi is the occupancy range ($\mathbb{N}$ versus ${0,1}$). That restriction is Pauli exclusion, justified in RS by the exchange phase $-1$ at the half-cycle; after the fork the algebra is free of further physical input.
proof idea
Establish the elementary bounds $0 < e^{-t} < 1$ and the nonzero denominators $1 - e^{-t}$ and $e^t - 1$. Record the product identity $e^{-t}, e^{t} = 1$. Rewrite the left-hand side by replacing the weighted sum with the closed form from bose_weighted_hasSum (via tsum_eq) and the bare partition sum with bose_partition_tsum. After field_simp, a single linear_combination against the product identity yields $1/(e^t - 1)$.
why it matters
This is the Bose half of the occupation-number layer that the module advertises: $\langle n\rangle = 1/(e^t \mp 1)$. Downstream, bose_energy_kernel_eq rewrites the Bose energy integrand $t^3/(e^t - 1)$ as $t^3$ times this occupation ratio, so the thermal energy density inherits a partition-function origin rather than an ansatz. The certificate partitionKernelsCert bundles the claim with the matching Fermi occupation and the log-kernel identities, feeding the loop's axiom audit.
In the broader RS cosmology chain the result sits under phase-space reduction and the thermal-history integrals; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it supplies the standard Bose floor those later integrals assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.