boltzmannWeight_pow

The StatisticsKernels module rebuilds the Bose and Fermi pressure and energy kernels from a single-mode grand partition function at vanishing chemical potential. The only microscopic input is the Gibbs weight of an $n$-quanta occupancy at dimensionless energy $t = E/T$.

That weight is defined by $w_n(t) := e^{-n t}$. The one-quantum factor is therefore $w_1(t) = e^{-t}$. Writing $w_n$ as a pure power of $w_1$ is the algebraic step that turns the bosonic sum $\sum_n w_n$ into a geometric series in $x = e^{-t}$.

Upstream, boltzmannWeight is exactly this definition: Real.exp (-(n * t)). No positivity or temperature hypothesis is required for the power identity itself.

Term-mode proof in three steps. Unfold the definition $w_n(t) = e^{-(n t)}$. Rewrite via Real.exp_nat_mul in the reverse direction, which supplies $e^{n \cdot (-t)} = (e^{-t})^n$. Finish with ring_nf to match the scalar arithmetic in the exponents. No case split on $n$ or $t$ is needed.

This identity is the bridge from the microstate weight to closed-form Bose kernels. Downstream, bosePartition_eq rewrites the unrestricted occupancy sum as $\sum_n x^n$ with $x = e^{-t}$ and invokes the geometric-series tsum to obtain $Z_B = (1 - e^{-t})^{-1}$. The same rewrite feeds boseOccupation_eq, which evaluates the weighted mean $\langle n \rangle_B = 1/(e^t - 1)$ via $\sum n x^n = x/(1-x)^2$.

In the module ledger these partition and occupation theorems discharge the MODEL status previously attached to the Bose pressure kernel $-\ln(1-e^{-t})$ and the energy kernel $t/(e^t-1)$ in PhaseSpaceReduction. The present lemma is the elementary exponential identity those geometric-series arguments rest on. It does not itself touch the Recognition forcing chain (T0–T8) or the $\phi$-ladder; it sits in the cosmology statistics layer that supplies thermodynamic kernels to the plasma and $\eta_B$ arguments.