fermi_partition_two_state
plain-language theorem explainer
The single-mode Fermi grand partition function collapses to two terms: Z_F(t) = 1 + e^{-t}, because Pauli occupancy is only {0,1}. Cosmology and statistical-mechanics proofs that need the closed form of the fermionic mode sum cite this identity. The proof is a one-line simplification expanding the Fin 2 sum.
Claim. For every real $t$, $\sum_{n\in\{0,1\}} (e^{-t})^n = 1 + e^{-t}$.
background
This module builds the statistical-mechanics floor under the cosmology thermal-history chain: per-mode grand partition functions for Bose and Fermi modes, the log kernels consumed by phase-space reduction, and mean occupation numbers. Everything is written in the variable $x = e^{-t}$ with $t > 0$, so $0 < x < 1$ and series converge.
The sole physical fork between Bose and Fermi is the occupancy range. For fermions, Pauli exclusion (justified in RS by the exchange phase $-1$ at the half-cycle, re-exported as the fermionic exchange sign) forces occupancy in ${0,1}$. Indexing the sum by Fin 2 encodes that restriction as a choice of statement, not a hidden axiom. After that fork the algebra is free of further physical input.
Downstream, the Fermi log kernel used in phase-space reduction is defined as $\ln(1+e^{-t})$. The present identity is the bridge from the occupancy sum to that closed form.
proof idea
One-line tactic proof. simp with the Mathlib lemma that expands a sum over Fin 2 into the two explicit summands $n=0$ and $n=1$. The $n=0$ term is $1$ and the $n=1$ term is $e^{-t}$, which is the claimed right-hand side. No analysis or convergence argument is required.
why it matters
Parent theorem fermiLogKernel_from_partition rewrites $\log$ of this sum and identifies it with PhaseSpaceReduction.fermiLogKernel. That identification is the Fermi half of the module's main deliverable: the log kernels that feed radiation entropy and phase-space reduction in the cosmology chain.
In the Recognition framework the only RS-specific input is the occupancy restriction itself (exchange phase $-1$ from the eight-tick / spin-statistics key). Once occupancy is ${0,1}$, $Z_F = 1+e^{-t}$ and $\log Z_F = \ln(1+e^{-t})$ are pure mathematics. The companion Bose identities run in parallel with geometric series over $\mathbb{N}$. Together they underwrite the occupation numbers $\langle n\rangle = 1/(e^t \mp 1)$ used in the thermal-history stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.