boltzmannWeight
plain-language theorem explainer
Defines the zero-chemical-potential Gibbs weight of an n-quanta microstate at dimensionless energy t = E/T: w_n = exp(−n t). Cosmology and statistical-mechanics developments that build single-mode Bose and Fermi partition functions cite it as the common microstate weight. The body is a one-line Real.exp definition.
Claim. For real $t$ and natural number $n$, the Gibbs weight of the $n$-quanta microstate at dimensionless energy $t = E/T$ (equivalently $\beta E$), with chemical potential zero, is $w_n(t) := e^{-n t}$.
background
The StatisticsKernels module rebuilds the Bose and Fermi pressure and energy kernels that PhaseSpaceReduction previously took as model inputs. The only microscopic ingredients are the Gibbs weight of an $n$-quanta microstate and the allowed occupancy sets: unrestricted $n \in \mathbb{N}$ for bosons, and $n \in {0,1}$ for fermions (Pauli exclusion), all at $\mu = 0$.
Dimensionless energy is $t = E/T$. The weight $w_n = e^{-n t}$ is the Boltzmann factor of that microstate. Summing it over the occupancy set yields the single-mode grand partition function $Z_{\mathrm{mode}}$; pressure kernels are then $\ln Z$, mean occupations are ensemble averages $\langle n \rangle = (\sum n w_n)/Z$, and energy kernels are $t\langle n \rangle$.
This definition is the shared atomic weight under those sums. Downstream lemmas also record that it is the $n$-th power of the one-quantum weight $e^{-t}$.
proof idea
Pure definition: the body is Real.exp (-(n * t)). No lemmas are applied. Downstream proofs typically unfold this name, then rewrite with Real.exp_nat_mul (or the dedicated power lemma) to treat the weight as a geometric term $(e^{-t})^n$.
why it matters
Every single-mode Bose/Fermi object in this module is built on this weight: the bosonic and fermionic partition functions sum it; the occupation numbers weight $n$ by it and normalize by $Z$; the power lemma rewrites it as $(e^{-t})^n$ for geometric-series arguments. Those identities feed the theorems that recover the Bose–Einstein and Fermi–Dirac distributions, identify the log kernels with $\ln Z$, and relate energy kernels to $t\langle n \rangle$.
In the broader Recognition cosmology chain this closes the provenance gap noted in the module doc: plasma pressure and energy along the $\eta_B$ line no longer start from ad-hoc kernels but from $\sum e^{-n E/T}$ in momentum space. It is scaffolding for thermodynamic consistency ($\langle n \rangle = -\partial_t \ln Z$), not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.