mode_energy_fermi
plain-language theorem explainer
Mean energy of one fermionic mode equals minus the β-derivative of its log partition function: −∂_β ln Z_F(βE) = E·⟨n⟩_F(βE). Anyone matching Fermi pressure kernels to energy densities in the grand-canonical setup cites this. Proof is chain rule on the log-kernel, then rewrite via ln Z_F = pressure kernel.
Claim. For all real $E$ and inverse temperature $\beta$, the map $b \mapsto \ln Z_F(b E)$ is differentiable at $\beta$ with derivative $-(E\, n_F(\beta E))$, where $Z_F(t)=1+e^{-t}$ is the two-state fermionic partition function and $n_F(t)=1/(e^{t}+1)$ is the Fermi–Dirac mean occupation.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure kernels $\mp\ln(1\mp e^{-t})$ and energy kernels $t/(e^{t}\mp 1)$ from a single-mode grand partition function at $\mu=0$, instead of taking them as model inputs. Fermions are restricted to occupancies ${0,1}$ (Pauli), so $Z_F(t)=1+e^{-t}$ with dimensionless $t=E/T$ (equivalently $t=\beta E$).
Upstream, the Fermi pressure kernel $\ln(1+e^{-t})$ from PhaseSpaceReduction is identified with $\ln Z_F$ (fermiLogKernel_eq_log_partition). The Fermi–Dirac occupation is the ensemble mean $\langle n\rangle_F=1/(e^{t}+1)$. Grand-canonical thermodynamics then requires the mode energy identity $\langle E\rangle=-\partial_\beta\ln Z$, which is the content of this theorem (module item 5: thermodynamic consistency of the kernels).
proof idea
First, $b\mapsto b\cdot E$ has derivative $E$ at $\beta$ (identity times constant). Compose with the known derivative of the Fermi log-kernel at $\beta E$ (fermiLogKernel_hasDerivAt), which contributes a factor $-n_F(\beta E)$. Convert the composite slope by a one-line ring identity to $-(E\cdot n_F(\beta E))$. Finally apply derivative congruence: the log-kernel equals $\ln Z_F$ everywhere (fermiLogKernel_eq_log_partition), so the same derivative holds for $b\mapsto\ln(\mathrm{fermiPartition}(b E))$.
why it matters
Closes the Fermi half of thermodynamic consistency in this module: pressure and energy kernels are not independent MODEL inputs but are linked by $\langle E\rangle=-\partial_\beta\ln Z$ exactly as grand-canonical formalism demands. It sits beside the Bose twin and supports the capstone story that plasma pressure/energy in the $\eta_B$ chain start from $\sum e^{-n E/T}$ in momentum space, with energy densities read off occupations.
No downstream used_by edges yet; it is a proved leaf ready for radiation/plasma integrals. Framework role is continuum statistical mechanics under Cosmology, not a T0–T8 forcing step. It makes the Fermi log-kernel and occupation interchangeable under $\beta$-differentiation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.