fermiLogKernel_from_partition
plain-language theorem explainer
The logarithm of the two-state fermionic grand partition function equals the Fermi pressure kernel ln(1+e^{-t}). Cosmology and thermal-history arguments that import the phase-space reduction layer cite this to replace the abstract kernel by an explicit mode sum. The proof is a two-step rewrite: the Fin-2 sum collapses to 1+e^{-t}, matching the kernel definition.
Claim. For every real $t$, $\log\bigl(\sum_{n\in\{0,1\}} (e^{-t})^n\bigr) = \ln(1+e^{-t})$.
background
In the per-mode grand-partition setting of this module, a fermionic mode is restricted by Pauli exclusion to occupancy in ${0,1}$. With $x=e^{-t}$, the single-mode partition function is the two-term sum $Z_F=\sum_{n:\mathrm{Fin},2}x^n$. The module works with $0<t$ so $0<x<1$ and every series converges; the identity itself is algebraic for all real $t$ where the log is defined.
Upstream, the two-state evaluation records $Z_F(t)=1+e^{-t}$. The phase-space reduction layer defines the Fermi pressure kernel as $\ln(1+e^{-t})$, the quantity that enters thermal integrals for fermionic radiation. A parallel complex-valued copy appears in the radiation-entropy Mellin machinery.
The only physical fork between Bose and Fermi here is the occupancy range. The exchange phase $-1$ from the eight-tick spin-statistics key justifies the $\mathrm{Fin},2$ index as a choice of statement; after that fork the algebra carries no further RS input.
proof idea
One-line rewrite proof. Apply the two-state partition lemma to replace $\sum_{n:\mathrm{Fin},2}e^{-tn}$ by $1+e^{-t}$. Unfold the definition of the phase-space Fermi log kernel, which is exactly $\log(1+e^{-t})$. Both sides agree.
why it matters
This lemma is the fermionic half of the partition-kernel certificate, which bundles the identities that the log kernels used upstream equal the logs of the derived partition functions, together with the Bose-Einstein and Fermi-Dirac occupation formulas. That certificate is consumed by the loop axiom audit (#print axioms must show only the base three).
In the RS cosmology chain it anchors the fermionic side of the statistical-mechanics floor beneath the thermal-history integrals. The Pauli occupancy restriction traces to the eight-tick exchange sign, so the result sits at the junction of the foundation spin-statistics key and the cosmology radiation layer. It does not itself force $D=3$ or the eight-tick period; those enter elsewhere in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.