fermiPartition
plain-language theorem explainer
The fermionic single-mode grand partition at dimensionless energy $t=E/T$ is the two-state sum of Gibbs weights over Pauli-allowed occupancies $n\in\{0,1\}$. Cosmology and statistical-mechanics proofs cite it as the starting object for Fermi pressure, occupation, and mode energy. The body is the finite sum of Boltzmann weights; closed form and positivity are separate lemmas.
Claim. For $t\in\mathbb{R}$, the fermionic single-mode grand partition function (chemical potential zero) is $Z_F(t)=\sum_{n=0}^{1}e^{-n t}$, i.e. the sum of Gibbs weights over the Pauli-restricted occupancies $\{0,1\}$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure kernels $\mp\ln(1\mp e^{-t})$ and energy kernels $t/(e^t\mp 1)$ from a single-mode grand partition at $\mu=0$, rather than taking those kernels as primitive MODEL inputs. The only ingredients are the Gibbs weight of an $n$-quanta microstate and the allowed occupancy set.
Upstream, the Boltzmann weight is $w_n(t)=e^{-n t}$ for dimensionless $t=E/T$. Bosons sum over all $n\in\mathbb{N}$; fermions are restricted by Pauli exclusion to $n\in{0,1}$. This definition is exactly that two-term sum. The module then proves $Z_F=1+e^{-t}$, identifies the Fermi log-kernel with $\ln Z_F$, and recovers the Fermi–Dirac mean occupation as $(\sum n,w_n)/Z_F$.
proof idea
Pure definition: unfold to the Finset sum of Boltzmann weights over range 2, i.e. the two terms $n=0$ and $n=1$. No lemmas are applied at the definition site; algebraic simplification to $1+e^{-t}$ is deferred to the companion equality theorem.
why it matters
This is the fermionic half of the partition-function foundation for the module. Downstream, the equality theorem closes $Z_F(t)=1+e^{-t}$; positivity follows immediately; the Fermi occupation is the weighted mean over the same two states divided by $Z_F$; and the log-kernel identity states that the Fermi pressure kernel is literally $\ln Z_F$.
The mode-energy theorem then gives the textbook relation $-\partial_\beta\ln Z_F(\beta E)=E\langle n\rangle_F$. The capstone plasmaPressure_from_partitionFunction integrates $T\ln Z_F(E/T)$ (and the Bose twin) over phase space, so plasma pressure in the $\eta_B$ chain starts from Gibbs weights and occupancy sets alone, with no independent log-kernel inputs. That is the module's stated provenance goal for cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.