fermiEnergyKernel
plain-language theorem explainer
Defines the Fermi energy kernel $K_F(t)=t/(e^t+1)$, the radial integrand factor for fermionic energy density in momentum space. Cosmology and statistical-mechanics proofs cite it when reducing 3D phase-space integrals to the standard $T^4$ plasma energy. The body is a one-line closed-form definition, not a derived equality.
Claim. The Fermi energy kernel is the real function $K_F(t) = \frac{t}{e^{t}+1}$ for $t \in \mathbb{R}$.
background
The module PhaseSpaceReduction starts from the 3D momentum integral for plasma pressure and energy, $P = (g/(2\pi)^3)\int d^3k, T,K(|k|/T)$, and derives the reduced 1D form with prefactor $g/(2\pi^2)$ and $T^4$ scaling. That angular factor comes from co-area reduction in $D=3$ (unit-ball volume $4\pi/3$), and the Stefan–Boltzmann exponent $4$ is $D+1$ with $D=3$ forced upstream by T8.
Sibling kernels split Bose and Fermi statistics: log-kernels for pressure (grand potential) and energy kernels for $\langle E\rangle$. The Fermi energy kernel is the factor that multiplies the radial measure after the substitution $k=T t$. Downstream, StatisticsKernels identifies it with $t$ times the Fermi–Dirac occupation $1/(e^t+1)$, and with $-t,\partial_t\ln Z_F$.
proof idea
Definitional: the body is the explicit formula $t/(\exp t + 1)$. No tactics, no lemmas. Downstream equalities (occupation form, derivative of the Fermi log-kernel) are proved elsewhere by unfolding this def and algebraic rearrangement.
why it matters
This kernel is the fermionic half of the energy-side phase-space reduction. plasmaEnergy_from_phaseSpace rewrites the sum of Bose and Fermi 3D densities as GrandPotential.plasmaEnergy by unfolding this def after radial reduction. phaseSpaceEnergy_closed_form then quotes the classical closed form $(\pi^2/30)(g_B+(7/8)g_F)T^4$.
In StatisticsKernels it is the bridge from partition-function calculus: fermiEnergyKernel_eq_occupation and fermiEnergyKernel_from_logKernel show $K_F(t)=t\langle n\rangle_F=-t,(\mathrm{d}/\mathrm{d}t)\ln Z_F$, so the capstone plasmaEnergy_from_occupation can replace energy kernels by $E\langle n\rangle$ without changing the integral. Framework link: the $T^4$ power and $1/(2\pi^2)$ prefactor are not model inputs; they follow from $D=3$ (T8) plus Haar co-area, with this kernel supplying the Fermi statistics factor inside that derived skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.