fermi_occupation
plain-language theorem explainer
The mean occupancy of a two-state fermionic mode equals the Fermi–Dirac factor 1/(e^t+1). Cosmology and thermal-history proofs cite it to replace the explicit ratio of finite sums by the closed FD form. The proof expands the Fin-2 sums, clears denominators, and cancels via exp(−t)·exp(t)=1.
Claim. For every real $t$, the mean occupation of a Pauli-restricted mode is $$\frac{\sum_{n\in\{0,1\}} n\,e^{-nt}}{\sum_{n\in\{0,1\}} e^{-nt}} = \frac{1}{e^{t}+1}.$$
background
This module builds the statistical-mechanics floor under the cosmology thermal-history chain: per-mode grand partition functions, the log kernels consumed by phase-space reduction, and the mean occupation numbers $\langle n\rangle=1/(e^{t}\mp 1)$. Everything is written in the variable $x=e^{-t}$ (with $0<t$ so $0<x<1$ and series converge).
For fermions the occupancy set is ${0,1}$ by the Pauli principle. The module treats that restriction as the choice of index type Fin 2, justified by the exchange phase $-1$ at the half-cycle (the eight-tick spin-statistics key) plus the standard antisymmetrization argument: a doubly occupied antisymmetric state is its own negative, hence zero. The only physical fork versus the Bose case is that occupancy range; after the fork the algebra is free of further RS input.
The Fermi partition function is therefore the two-term sum $Z_F=1+x$, and the occupation number is the weighted average $\langle n\rangle=(\sum n,x^n)/(\sum x^n)$.
proof idea
Positivity of $e^{-t}$ and $e^{t}$ gives nonzero denominators $1+e^{-t}$ and $e^{t}+1$. The key algebraic identity is $e^{-t}\cdot e^{t}=1$ (via Real.exp_add). Expand both finite sums over Fin 2 to the explicit two-term expressions $0\cdot 1+1\cdot e^{-t}$ over $1+e^{-t}$, simplify the arithmetic, clear fields, and finish by linear combination against the product identity, yielding $1/(e^{t}+1)$.
why it matters
This is the Fermi half of the occupation-number layer that the module certificate bundles with the Bose case and the log-kernel identities. Downstream, fermi_energy_kernel_eq rewrites the Fermi energy integrand $t^3/(e^t+1)$ as $t^3$ times this occupation ratio, so the thermal-history energy density can cite the closed FD form rather than the raw two-state sum. The sibling certificate partitionKernelsCert packages both occupation theorems for the loop axiom audit (only the base three axioms).
In the broader RS picture the result sits under the cosmology chain that feeds phase-space reduction. The Pauli occupancy bound itself is not re-proved here; it enters as the statement choice justified by the eight-tick exchange sign. No free parameter remains after that fork: the closed form is pure finite algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.