fermiLogKernel
plain-language theorem explainer
Defines the real Fermi pressure kernel $\ln(1+e^{-t})$, the single-mode log of the two-state Fermi grand partition function. Cosmology and statistical-mechanics proofs cite it as the fermionic integrand in 3D phase-space pressure and energy. The body is a one-line closed-form definition, not a derived identity.
Claim. For each real $t$, the Fermi logarithmic pressure kernel is $\ln(1+e^{-t})$.
background
The module PhaseSpaceReduction derives the plasma pressure prefactor $g/(2\pi^2),T^4$ from the underlying 3D momentum integral $P=(g/(2\pi)^3)\int d^3k,T,K(|k|/T)$, using radial co-area reduction and the substitution $k=T t$. The Stefan–Boltzmann $T^4$ scaling is $D+1$ with $D=3$ forced upstream (T8).
In that setting the radial integrand splits into Bose and Fermi log kernels. The Fermi kernel is the pressure contribution of a fermionic mode: after angular reduction one integrates $t^2\ln(1+e^{-t})$ (up to constants). A parallel complex-valued copy appears in RadiationEntropyRelation for Mellin analysis; the real form here is the one fed to phase-space density.
Downstream, PartitionKernels identifies $\ln Z_F$ with this kernel: Pauli occupancy ${0,1}$ gives $Z_F(t)=1+e^{-t}$, so $\log Z_F=\ln(1+e^{-t})$.
proof idea
Pure definition: the body is Real.log (1 + Real.exp (-t)). No lemmas or tactics. Sibling boseLogKernel is the Bose analogue $-\ln(1-e^{-t})$; energy kernels are the occupation-weighted variants.
why it matters
Anchors the fermionic half of the phase-space pressure chain. plasmaPressure_from_phaseSpace rewrites the 3D integral with boseLogKernel and fermiLogKernel into the previously definitional GrandPotential.plasmaPressure. phaseSpacePressure_closed_form then yields the Stefan–Boltzmann law $(\pi^2/90)(g_B+(7/8)g_F)T^4$ with the fermionic $7/8$ factor. phaseSpacePressure_potential differentiates that pressure to radiation entropy, closing the Euler chain $\rho=Ts-P$.
PartitionKernels certifies the microcanonical origin: fermiLogKernel_from_partition and partitionKernelsCert equate the kernel to $\log$ of the two-state Fermi sum, so the continuum integrand is not an ad-hoc fit. In the RS ledger this is the fermionic pressure kernel sitting under the $D=3$ forcing and the derived $g/(2\pi^2)$ angular factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.