bose_partition_tsum
plain-language theorem explainer
For any positive temperature parameter t, the bosonic single-mode grand partition function equals the closed geometric sum (1 - e^{-t})^{-1}. Cosmology and statistical-mechanics proofs cite this to replace the occupancy series by its closed form. The proof is a one-line extraction of the sum value from the already-proved HasSum statement for the same series.
Claim. For every real $t > 0$, $\sum_{n=0}^{\infty} e^{-t n} = (1 - e^{-t})^{-1}$.
background
The module derives per-mode grand partition functions and occupation numbers that sit under the cosmology thermal-history chain. Everything is written in the variable $x = e^{-t}$ with $t > 0$, so $0 < x < 1$ and every geometric series converges absolutely.
For a bosonic mode the occupancy runs over all of $\mathbb{N}$. The Boltzmann-weighted sum is therefore the ordinary geometric series $Z_B = \sum_{n} x^n$. The companion theorem bose_partition_hasSum already records that this series HasSum to $(1-x)^{-1}$, via Mathlib's geometric-series criterion once $|x| < 1$ is checked from $t > 0$.
Downstream, the Bose log-kernel used in phase-space reduction and radiation entropy is defined as $-\log(1-e^{-t})$. Identifying $\log Z_B$ with that kernel requires the closed form of the tsum, which is exactly what this declaration supplies.
proof idea
One-line term proof. Apply the tsum_eq field of the HasSum witness produced by bose_partition_hasSum t ht. That upstream lemma already proves absolute convergence of $n \mapsto e^{-t n}$ and identifies the sum as $(1-e^{-t})^{-1}$ by reducing to Mathlib's hasSum_geometric_of_norm_lt_one after checking $0 < e^{-t} < 1$. No further algebraic work is done here.
why it matters
This is the bridge from the series definition of the Bose partition function to the closed form used everywhere upstream in cosmology. The immediate parent boseLogKernel_from_partition rewrites $\log(\sum e^{-tn})$ via this identity and Real.log_inv, proving that PhaseSpaceReduction.boseLogKernel is no longer a definitional choice but the logarithm of the derived $Z_B$. The sibling bose_occupation likewise divides the weighted tsum by this partition tsum to obtain the Bose-Einstein mean occupancy $1/(e^t-1)$.
In the Recognition Science floor, the only physical input at this stage is the occupancy range $\mathbb{N}$ versus ${0,1}$ (Pauli), justified by the exchange-sign half-cycle; after that fork the geometry of the series is pure mathematics. Closing the partition-to-kernel identification removes a free definition from the pressure and entropy integrals in the thermal-history chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.