number_integrand_fermi
plain-language theorem explainer
The fermion number density integrand equals t squared times the Fermi–Dirac mean occupation: t²/(eᵗ+1). Cosmologists and statistical-mechanics workers cite it when assembling the dimensionless number integral that evaluates to (3/2)ζ(3). The proof is a one-line rewrite of the occupation identity followed by ring normalization.
Claim. For every real $t$, $t^{2}\,\langle n\rangle_{F}(t)=t^{2}/(e^{t}+1)$, where $\langle n\rangle_{F}(t)$ is the ensemble-mean occupation of a single fermionic mode at dimensionless energy $t=E/T$.
background
The StatisticsKernels module rebuilds the standard Bose/Fermi pressure and energy kernels from the grand partition function of one mode at vanishing chemical potential. The only inputs are the Gibbs weight $e^{-n t}$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, and $n\in{0,1}$ for fermions (Pauli exclusion). Dimensionless energy is $t=E/T$.
Mean fermionic occupation is defined as the two-state ensemble average $\langle n\rangle_{F}=(\sum_{n<2} n,w_{n})/Z_{F}$. Upstream, fermiOccupation_eq proves the closed form $\langle n\rangle_{F}=1/(e^{t}+1)$ with no convergence hypothesis, because the sum is finite. Multiplying by $t^{2}$ produces the standard number-density integrand whose momentum integral is proportional to $(3/2)\zeta(3)$.
proof idea
One-line term proof. Rewrite the left-hand side with the Fermi–Dirac identity $\langle n\rangle_{F}(t)=1/(e^{t}+1)$, then apply ring to clear the resulting algebraic identity $t^{2}\cdot(1/(e^{t}+1))=t^{2}/(e^{t}+1)$.
why it matters
In the Recognition cosmology stack, number and energy densities of relativistic species are assembled from phase-space integrals of occupation kernels. This identity packages the fermion number integrand as $t^{2}\langle n\rangle_{F}$, matching the classical form whose integral is $(3/2)\zeta(3)$. It sits downstream of the partition-function derivation of the Fermi–Dirac law and upstream of any plasma or relic-abundance bookkeeping that needs the number density rather than the energy density.
The module’s larger program replaces MODEL-level kernel definitions in PhaseSpaceReduction and GrandPotential by theorems that start from $\sum e^{-n E/T}$. Energy kernels are already identified with $t\langle n\rangle$; this lemma is the parallel packaging for number. No downstream Lean users are recorded yet, so it is presently a ready-to-cite algebraic bridge rather than a loaded dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.