bosePartition_pos
plain-language theorem explainer
For positive dimensionless temperature ratio t = E/T, the bosonic single-mode grand partition function Z_B(t) is strictly positive. Cosmology and statistical-mechanics developments that take logs or invert Z_B cite this positivity. The proof rewrites Z_B via the closed geometric form and uses e^{-t} < 1 to get a positive reciprocal.
Claim. For every real $t > 0$, the bosonic single-mode grand partition function $Z_B(t) = \sum_{n \in \mathbb{N}} e^{-n t}$ satisfies $Z_B(t) > 0$.
background
The module StatisticsKernels derives the Bose/Fermi pressure and energy kernels from the single-mode grand partition function at vanishing chemical potential, rather than taking those kernels as primitive MODEL inputs. The only data are Gibbs weights $e^{-n t}$ with $t = E/T$ and the occupancy sets: unrestricted $n \in \mathbb{N}$ for bosons, and ${0,1}$ for fermions.
The bosonic partition is defined as the series $Z_B(t) = \sum_{n} e^{-n t}$. Upstream, bosePartition_eq evaluates it by the geometric series: for $t > 0$, $Z_B(t) = (1 - e^{-t})^{-1}$. The comparison $e^{-t} < 1$ (from exp_neg_lt_one) is exactly the radius condition that makes the series converge and the closed form well-defined and positive.
proof idea
Rewrite $Z_B(t)$ with bosePartition_eq to obtain $(1 - e^{-t})^{-1}$. Invoke exp_neg_lt_one to get $e^{-t} < 1$, hence $1 - e^{-t} > 0$. Conclude positivity of the reciprocal by inv_pos and a one-line linarith on the denominator.
why it matters
Positivity of $Z_B$ is the elementary gate before taking $\ln Z_B$ (the Bose pressure kernel) and before thermodynamic identities such as $\langle n \rangle = -\partial_t \ln Z$. The module's provenance ledger aims to replace MODEL kernels in PhaseSpaceReduction and the $\eta_B$ plasma chain by quantities derived from $\sum e^{-n E/T}$. No downstream uses are wired yet in the graph, but sibling lemmas (boseLogKernel_eq_log_partition, occupation and energy identities, plasma capstones) all presuppose a positive partition so that logs and mean occupations are defined over $\mathbb{R}$. This is classical grand-canonical bookkeeping inside the RS cosmology stack, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.