bose_partition_hasSum
plain-language theorem explainer
For every real t > 0 the Bose single-mode grand partition series Σ_n exp(-t)^n converges, with sum (1 - exp(-t))^{-1}. Thermal-history and phase-space workers cite this as the HasSum certificate behind Z_B. The proof records 0 < exp(-t) < 1 and applies Mathlib's geometric-series summability lemma.
Claim. For every real $t > 0$, the series $\sum_{n \in \mathbb{N}} (e^{-t})^n$ is summable and equals $(1 - e^{-t})^{-1}$.
background
The module builds the statistical-mechanics floor under the cosmology thermal-history chain: per-mode grand partition functions for one bosonic and one fermionic mode, the log kernels consumed by phase-space reduction, and the mean occupations $\langle n \rangle = 1/(e^t \mp 1)$.
Everything is written in the variable $x = e^{-t}$ with $t > 0$, so $0 < x < 1$ and every series converges. For a Bose mode the occupancy runs over all of $\mathbb{N}$, so the Boltzmann-weighted sum is the geometric series $Z_B = \sum_n x^n = (1-x)^{-1}$. The only physical fork versus Fermi is that occupancy range; after the choice of index type the rest is pure analysis.
The classical geometric-series summability fact (norm of the ratio strictly less than one) is the analytic engine; no Recognition-specific cost or ladder structure enters this lemma.
proof idea
Short tactic proof. First obtain $0 < e^{-t}$ from positivity of the exponential. Next obtain $e^{-t} < 1$ from the characterization of when the exponential is less than one, using $t > 0$ via linear arithmetic. Apply Mathlib's hasSum_geometric_of_norm_lt_one. Rewrite the real norm as absolute value and drop the absolute value by positivity of $e^{-t}$. The remaining goal is exactly $e^{-t} < 1$.
why it matters
This is the summability certificate for the Bose partition function. The immediate parent is the tsum form $Z_B(t) = (1-e^{-t})^{-1}$, obtained by reading off the sum from HasSum; that equality is what licenses identifying $\log Z_B$ with the Bose log kernel used in phase-space reduction (pressure and entropy integrals).
In the module hierarchy it sits at the start of the Bose branch of the per-mode grand-partition development. Downstream occupation numbers $\langle n \rangle = 1/(e^t - 1)$ and the cosmology thermal-history chain depend on having a rigorously summed $Z_B$. No forcing-chain landmark (T5–T8) is invoked here; the lemma is ordinary real analysis placed so the RS thermal stack has a clean Bose base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.