fermiPartition_eq
plain-language theorem explainer
The fermionic single-mode grand partition function equals $1+e^{-t}$ for every real $t$. Cosmology and statistical-mechanics arguments that start from Pauli-restricted occupancy cite this closed form. The proof unfolds the two-state sum of Gibbs weights and evaluates the finite range sum.
Claim. For every real $t$, the fermionic single-mode grand partition function (sum of Gibbs weights over occupancy $n\in\{0,1\}$) equals $1+e^{-t}$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from the grand partition function of a single mode at vanishing chemical potential. Dimensionless energy is $t=E/T$. The only inputs 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).
The Gibbs weight is $w_n(t)=e^{-n t}$. The fermionic partition is defined as the two-term sum $Z_F(t)=\sum_{n=0}^{1} w_n(t)$. Upstream, PhaseSpaceReduction and GrandPotential treated $\ln(1+e^{-t})$ and related kernels as model inputs; this module derives them from $\sum e^{-n t}$.
proof idea
Unfold the definitions of the fermionic partition and the Boltzmann weight, so the claim is the finite sum $\sum_{n\in{0,1}} e^{-n t}=1+e^{-t}$. Apply the successor rule for sums over Finset.range to expand the two terms: $n=0$ contributes $e^{0}=1$, and $n=1$ contributes $e^{-t}$. Algebraic simplification finishes the identity. No convergence hypothesis is needed.
why it matters
This is the fermionic half of step 1 in the module ledger: closed-form partition functions from occupancy sums. Downstream, fermiLogKernel_eq_log_partition rewrites the Fermi pressure kernel as $\ln Z_F$ by substituting this identity; fermiOccupation_eq obtains the Fermi–Dirac mean occupation $1/(e^{t}+1)$ from the same closed form; and fermiPartition_pos gets strict positivity by rewriting and a positivity tactic.
Together these discharge the MODEL status of the Fermi log and energy kernels used in the plasma pressure/energy chain, so those quantities start from $\sum e^{-n E/T}$ rather than from postulated formulas. The result is pure single-mode statistical mechanics at $\mu=0$; it does not itself invoke the RS forcing chain (T0–T8), but it supplies the fermionic kernel layer those cosmology constructions consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.