bosePartition_eq
plain-language theorem explainer
For positive dimensionless energy t = E/T, the bosonic single-mode grand partition function equals (1 − e^{−t})^{-1}. Cosmology and statistical-mechanics arguments that start from Σ_n e^{−n t} cite this closed form. The proof rewrites the summand as a geometric ratio and applies Mathlib's geometric tsum under the strict contraction e^{−t} < 1.
Claim. For every real $t > 0$, the bosonic single-mode grand partition function $Z_B(t) := \sum_{n \in \mathbb{N}} e^{-n t}$ equals $(1 - e^{-t})^{-1}$.
background
This module sits in the cosmology statistics layer. Earlier work (PhaseSpaceReduction, GrandPotential) treated the Bose pressure kernel $-\ln(1-e^{-t})$ and energy kernel $t/(e^t-1)$ as model inputs. Here those kernels are derived from the single-mode grand partition function at vanishing chemical potential, with dimensionless energy $t = E/T$.
The bosonic partition is the unrestricted occupancy sum $Z_B(t) = \sum_{n\in\mathbb{N}} w(t,n)$, where the Gibbs weight is $w(t,n) = e^{-n t}$. The sibling lemma boltzmannWeight_pow records that this weight is exactly the $n$-th power of the one-quantum factor $e^{-t}$. For $t > 0$ one also has $e^{-t} < 1$, so the geometric series converges in $\mathbb{R}$.
The local goal is the classical closed form of that series, which then feeds log-partition, occupation, and energy identities used by the plasma pressure/energy chain.
proof idea
Term-mode proof. Unfold the definition of the bosonic partition to expose the tsum of Boltzmann weights. Rewrite each weight via boltzmannWeight_pow as $(e^{-t})^n$. Apply Mathlib's tsum_geometric_of_lt_one with nonnegativity of $e^{-t}$ (from Real.exp_pos) and the strict bound $e^{-t} < 1$ from exp_neg_lt_one ht. The geometric sum formula yields $(1 - e^{-t})^{-1}$.
why it matters
This is step 1 of the module's derivation program: partition functions from occupancy sums. Downstream, boseLogKernel_eq_log_partition rewrites the former model pressure kernel as $\ln Z_B$, so $-\ln(1-e^{-t}) = \ln Z_B(t)$. boseOccupation_eq divides the weighted geometric series by this $Z_B$ to obtain the Bose–Einstein law $\langle n\rangle_B = 1/(e^t-1)$. bosePartition_pos uses the same closed form to prove positivity needed for logs and thermodynamic derivatives.
In the broader Recognition cosmology stack, plasma pressure and energy along the $\eta_B$ chain are thereby grounded in $\sum e^{-n E/T}$ rather than postulated kernels. The result is ordinary grand-canonical bookkeeping; its role is provenance, not a new physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.