fermiOccupation
plain-language theorem explainer
Defines the mean occupation number of a single fermionic mode at dimensionless energy t = E/T as the ensemble average ⟨n⟩ = (Σ_{n=0,1} n w_n)/Z_F. Cosmology and statistical-mechanics arguments cite it as the primitive from which the Fermi–Dirac distribution and energy kernels are derived. The body is a direct two-state weighted sum over Gibbs weights, normalized by the fermionic partition function.
Claim. For dimensionless energy $t \in \mathbb{R}$, the mean occupation of a fermionic mode is $\langle n \rangle_F(t) = \bigl(\sum_{n \in \{0,1\}} n\, e^{-n t}\bigr) / Z_F(t)$, where $Z_F(t) = \sum_{n \in \{0,1\}} e^{-n t}$ is the two-state grand partition function at vanishing chemical potential.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels that PhaseSpaceReduction previously took as MODEL inputs. The only primitives are the Gibbs weight $w_n = e^{-n t}$ of an $n$-quanta microstate at $t = E/T$ ($\mu = 0$) and the allowed occupancy sets: unrestricted $n \in \mathbb{N}$ for bosons, Pauli-restricted $n \in {0,1}$ for fermions.
Upstream, boltzmannWeight t n is exactly $e^{-n t}$, and fermiPartition t is the two-term sum $\sum_{n<2} e^{-n t}$. The mean occupation is the standard grand-canonical ratio $(\sum n, w_n)/Z$. Module goals include showing this equals the Fermi–Dirac factor $1/(e^t+1)$, that the energy kernel is $t\langle n\rangle$, and that $\langle n\rangle = -d(\ln Z)/dt$.
proof idea
Definitional, not a proof. The body writes the ensemble mean as the finite sum over Finset.range 2 of $n$ times the Gibbs weight, divided by the fermionic partition function already defined in-module. No lemmas are applied; later theorems (fermiOccupation_eq, etc.) unfold this definition and simplify the two-term sum.
why it matters
This is the occupation primitive for the fermionic half of the statistics-kernel derivation chain. Downstream, fermiOccupation_eq evaluates it to the Fermi–Dirac law $1/(e^t+1)$; fermiOccupation_lt_one records the Pauli bound $\langle n\rangle_F < 1$; fermiEnergyKernel_eq_occupation identifies the energy kernel with $t\langle n\rangle_F$; fermiLogKernel_hasDerivAt and mode_energy_fermi establish grand-canonical consistency $\langle n\rangle = -d(\ln Z)/dt$ and $-\partial_\beta\ln Z_F = E\langle n\rangle$; number_integrand_fermi and plasmaEnergy_from_occupation feed the $\eta_B$ plasma integrals. Together these discharge the MODEL status of the Fermi kernels in PhaseSpaceReduction, so cosmological pressure/energy start from $\sum e^{-nE/T}$ rather than postulated closed forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.