bose_weighted_hasSum

This module builds the 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$, which forces $0 < x < 1$ and absolute convergence of the geometric series.

For a bosonic mode the occupancy runs over all of $\mathbb{N}$, so the partition function is $Z_B = \sum x^n = (1-x)^{-1}$. Mean occupancy is the ratio of the occupancy-weighted sum $\sum n x^n$ to $Z_B$. The classical closed form $\sum n x^n = x/(1-x)^2$ is exactly what this theorem records as a HasSum statement, so downstream code can divide two summed series without re-proving convergence.

The only RS-specific fork in the module is the occupancy range ($\mathbb{N}$ vs ${0,1}$), justified by the exchange sign at the half-cycle; after that choice the algebra is pure analysis.

Set $\xi = e^{-t}$. Positivity of the exponential gives $\xi > 0$; the hypothesis $t > 0$ and Real.exp_lt_one_iff give $\xi < 1$. The Mathlib lemma hasSum_coe_mul_geometric_of_norm_lt_one then supplies HasSum (fun n => n · ξ^n) (ξ/(1-ξ)^2) once $|\xi| < 1$. The norm identity reduces to $\xi$ itself because $\xi > 0$, so the bound is exactly $\xi < 1$. No further algebraic rewriting is needed.

Immediate consumer is bose_occupation, which forms the ratio $(\sum n x^n)/(\sum x^n)$ and simplifies it to the Bose–Einstein mean occupancy $1/(e^t - 1)$. That occupation number, together with the companion Fermi formula, is the statistical-mechanics floor used by PhaseSpaceReduction log-kernels in the cosmology thermal-history chain.

Within Recognition Science the derivation is deliberately thin: the only physical input is the bosonic occupancy range $\mathbb{N}$ (versus Pauli-restricted ${0,1}$ from the eight-tick exchange sign). Once that range is fixed, the weighted geometric sum is pure mathematics and closes the numerator half of the Bose occupation identity with no free parameters.