fermiPartition_pos
plain-language theorem explainer
The fermionic single-mode grand partition function is strictly positive for every real temperature parameter t. Anyone deriving Fermi pressure or occupation kernels from ln Z needs this to keep logarithms and normalizations well-defined. The proof rewrites Z_F via the closed form 1+e^{-t} and finishes by positivity.
Claim. For every real $t$, the fermionic single-mode grand partition function $Z_F(t)=\sum_{n\in\{0,1\}}e^{-n t}$ satisfies $Z_F(t)>0$. Equivalently, $1+e^{-t}>0$ for all $t\in\mathbb{R}$.
background
This module rebuilds the Bose/Fermi pressure kernels $\mp\ln(1\mp e^{-t})$ and energy kernels $t/(e^t\mp 1)$ from the grand partition function of one mode at $\mu=0$, rather than taking them as model inputs. The only ingredients are Gibbs weights $e^{-n t}$ with $t=E/T$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, Pauli-restricted $n\in{0,1}$ for fermions.
The fermionic partition is defined as the two-state sum $Z_F(t)=\sum_{n<2}e^{-n t}$. Upstream, fermiPartition_eq evaluates that sum to the closed form $Z_F(t)=1+e^{-t}$ for every real $t$. Positivity of $Z_F$ is the elementary analytic fact needed before one may form $\ln Z_F$ (the Fermi pressure kernel) or normalize occupation averages $\langle n\rangle=(\sum n,w_n)/Z_F$.
proof idea
One rewrite plus the positivity tactic. Apply the closed-form identity $Z_F(t)=1+e^{-t}$, then discharge $0<1+\exp(-t)$ by Mathlib's positivity (sum of a positive constant and a positive exponential).
why it matters
In the Statistics Kernels ledger, pressure kernels are identified with $\ln Z_{\mathrm{mode}}$ and occupations with ensemble means over $Z$. Strict positivity of $Z_F$ is the gate that makes those logarithms and normalizations legitimate for every real $t$, including the cold and hot limits used in the $\eta_B$ plasma chain.
No downstream theorem currently cites this lemma (used-by is empty), but it sits beside the Bose twin and the planned equalities fermiLogKernel_eq_log_partition and fermiOccupation_eq. Those steps convert the PhaseSpaceReduction MODEL kernels into derived grand-canonical objects, so the plasma pressure/energy capstones can start from $\sum e^{-nE/T}$ rather than from postulated $\ln(1+e^{-t})$ forms. Within Recognition Cosmology this is bookkeeping hygiene, not a new forcing step: it secures the thermodynamic side of the BIT/phase-space reduction stack once the occupancy sets are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.