fermiLogKernel_eq_log_partition
plain-language theorem explainer
The Fermi pressure kernel equals the log of the single-mode fermionic grand partition function: ln(1+e^{-t}) = ln Z_F(t) for every real t. Cosmology and statistical-mechanics arguments that previously took the log kernel as a MODEL input can now cite it as ln Z. The proof is a one-line rewrite via the closed form Z_F = 1+e^{-t}, then reflexivity.
Claim. For every real $t$, the Fermi pressure kernel $\ln(1+e^{-t})$ equals $\ln Z_F(t)$, where $Z_F(t)=\sum_{n\in\{0,1\}} e^{-n t}$ is the single-mode fermionic grand partition function at chemical potential zero.
background
This module rebuilds the Bose/Fermi pressure and energy kernels from the grand partition function of one mode at $\mu=0$, with dimensionless $t=E/T$. The only inputs are the Gibbs weight $e^{-n t}$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, Pauli-restricted $n\in{0,1}$ for fermions.
The Fermi log kernel was previously a bare definition in PhaseSpaceReduction: $\mathrm{fermiLogKernel}(t)=\ln(1+e^{-t})$. The fermionic partition is the two-state sum $Z_F(t)=\sum_{n<2} e^{-n t}$. Upstream, fermiPartition_eq closes that sum to $Z_F(t)=1+e^{-t}$ for every real $t$.
Identifying the pressure kernel with $\ln Z$ is the grand-canonical step that lets pressure and mean energy become derivative-related rather than independent MODEL inputs.
proof idea
Term-mode, two steps. Rewrite the right-hand side with fermiPartition_eq, which replaces $Z_F(t)$ by $1+e^{-t}$. Both sides are then definitionally $\ln(1+e^{-t})$ (the left by the definition of the Fermi log kernel), so rfl finishes.
why it matters
Closes item 2 of the module ledger for fermions: the previously-defined Fermi pressure kernel is literally $\ln Z_F$, not an independent input. Downstream, mode_energy_fermi uses the identification to prove the textbook relation $-\partial_\beta\ln Z_F(\beta E)=E\langle n\rangle_F(\beta E)$. The capstone plasmaPressure_from_partitionFunction rewrites plasma pressure in the $\eta_B$ chain as a phase-space integral of $T\cdot\ln Z_{\mathrm{mode}}(E/T)$, so only Gibbs weights and occupancy sets remain.
In the broader Recognition cosmology stack this discharges the MODEL tag on the Fermi log kernel inside phase-space reduction and grand-potential pressure, aligning the radiation sector with standard grand-canonical structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.