fermiOccupation_lt_one
plain-language theorem explainer
The mean occupation of a single fermionic mode is strictly less than one for every real dimensionless energy t. Workers on the RS plasma and phase-space chains cite this as the Pauli bound on average occupancy. The proof rewrites the ensemble mean to the closed Fermi–Dirac form 1/(e^t+1) and compares numerator against denominator using positivity of the exponential.
Claim. For every real $t$, the fermionic mean occupation satisfies $\langle n\rangle_F(t) < 1$. Equivalently, $1/(e^{t}+1) < 1$.
background
The StatisticsKernels module rebuilds the Bose and 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}$ of an $n$-quanta microstate and the allowed occupancy sets: $n\in\mathbb{N}$ for bosons, $n\in{0,1}$ for fermions (Pauli exclusion). Here $t=E/T$ is dimensionless.
The fermionic mean occupation is defined as the ensemble average $\langle n\rangle_F=(\sum_{n<2} n,w_n)/Z_F$ over the two-state sum. An upstream closed-form theorem identifies this average with the Fermi–Dirac distribution $\langle n\rangle_F=1/(e^{t}+1)$ for every real $t$, with no convergence hypothesis required.
The present bound is the elementary numerical consequence of that closed form: a mode whose microstates are only empty or singly occupied cannot have mean occupation one or larger.
proof idea
Rewrite the goal with the closed-form identity that $\mathrm{fermiOccupation},t=1/(e^{t}+1)$. Positivity of the real exponential supplies $e^{t}>0$, so the denominator $e^{t}+1$ is strictly larger than one. The inequality $1/(e^{t}+1)<1$ is then exactly the criterion for a positive-denominator quotient to be less than one, discharged by div_lt_one and a final linarith comparison.
why it matters
In the module ledger this is the Pauli bound: the statistical shadow of the occupancy restriction $n\in{0,1}$. It sits downstream of the derivation that the previously MODEL-tagged Fermi kernels are literally $\ln Z$ and $t\langle n\rangle$ for a two-state mode, so the bound is not an extra axiom but a corollary of the partition-function construction.
No parent theorem currently imports it (used-by is empty), yet it is the natural guardrail for any later estimate that treats fermionic mode sums, plasma pressure, or energy densities as strictly sub-saturated. Within Recognition Science it anchors the fermionic half of the statistics layer that feeds the $\eta_B$ cosmology chain, parallel to the bosonic occupation identities derived in the same file. It does not touch the forcing chain T0–T8 or the J-cost uniqueness step; its role is purely thermodynamic consistency of the fermionic sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.