fermiOccupation_eq
plain-language theorem explainer
The mean occupation of a single fermionic mode equals the Fermi–Dirac factor 1/(e^t+1) for every real t. Cosmology and statistical-mechanics arguments that need the closed form of ⟨n⟩_F cite this identity. The proof expands the two-state weighted sum, inserts Z_F = 1 + e^{-t}, and clears the resulting rational expression.
Claim. For every real $t$, the ensemble-mean occupation of a fermionic mode equals $\langle n\rangle_F(t) = 1/(e^{t}+1)$. Here the mean is the two-state ratio $(\sum_{n=0}^{1} n\,e^{-n t})/Z_F(t)$ with chemical potential zero and $t=E/T$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from a single-mode grand partition function at $\mu=0$, rather than taking those kernels as primitive MODEL inputs. The only data are the Gibbs weight $w_n=e^{-n t}$ of an $n$-quanta microstate and the allowed occupancies: $n\in\mathbb{N}$ for bosons, $n\in{0,1}$ for fermions (Pauli exclusion).
For fermions the partition function is the two-state sum $Z_F(t)=\sum_{n<2}e^{-n t}$. Upstream, fermiPartition_eq evaluates it to $Z_F=1+e^{-t}$ with no convergence hypothesis. Mean occupation is then defined as the normalized first moment $\langle n\rangle_F=(\sum_{n<2}n,w_n)/Z_F$. The present theorem closes that definition to the classical Fermi–Dirac factor.
Dimensionless energy $t=E/T$ is the sole argument; temperature and mode energy enter only through that ratio. The same pattern yields the Bose–Einstein factor from the unrestricted geometric series.
proof idea
Unfold the definitions of mean occupation and Gibbs weight, then rewrite the denominator via fermiPartition_eq so $Z_F=1+e^{-t}$. The numerator is a finite sum over Finset.range 2; simp with the usual range and arithmetic lemmas collapses it to the single term $e^{-t}$ (the $n=0$ contribution vanishes). After rewriting $e^{-t}=1/e^{t}$ and recording positivity of $1+e^{-t}$ and $e^{t}\neq 0$, field_simp clears the quotient to $1/(e^{t}+1)$.
why it matters
This is the Fermi half of the module's occupation-number step: once $\langle n\rangle_F$ is the closed Fermi–Dirac factor, every downstream kernel identity becomes an algebraic rewrite. It feeds fermiEnergyKernel_eq_occupation (energy kernel equals $t\cdot\langle n\rangle_F$), fermiLogKernel_hasDerivAt (grand-canonical consistency $d/dt,\ln(1+e^{-t})=-\langle n\rangle_F$), the Pauli bound $\langle n\rangle_F<1$, and the number integrand $t^2\langle n\rangle_F=t^2/(e^t+1)$ used in Fermi integrals.
In the broader Recognition cosmology stack these identities discharge the MODEL status of the Fermi pressure/energy kernels inherited from PhaseSpaceReduction, so plasma pressure and energy on the $\eta_B$ chain start from $\sum e^{-nE/T}$ rather than from postulated kernels. No forcing-chain landmark (T5–T8) is touched directly; the result is pure single-mode statistical mechanics inside the RS cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.