fermiEnergyKernel_from_logKernel
plain-language theorem explainer
For any real t, the Fermi energy kernel equals −t times the derivative of the Fermi log-pressure kernel: t/(e^t+1) = −t · (d/dt) ln(1+e^{−t}). Cosmology and statistical-mechanics proofs cite it to recover mean mode energy from the grand partition function. The proof rewrites via the known derivative of the log kernel and the occupation identity, then closes by ring.
Claim. For every real $t$, the Fermi energy kernel satisfies $$\frac{t}{e^{t}+1} = -t\,\frac{d}{dt}\ln\bigl(1+e^{-t}\bigr).$$ Equivalently, if $Z_F(t)=1+e^{-t}$ is the single-mode Fermi partition function at $\mu=0$ with $t=E/T$, then $t\,\langle n\rangle_F = -t\,(\ln Z_F)'(t)$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from the single-mode grand partition function at vanishing chemical potential. The only inputs are Gibbs weights $e^{-n t}$ with $t=E/T$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, $n\in{0,1}$ for fermions.
For fermions one obtains $Z_F=1+e^{-t}$. The Fermi log kernel is $\ln Z_F=\ln(1+e^{-t})$, previously taken as a MODEL definition in PhaseSpaceReduction. The Fermi energy kernel is $t/(e^t+1)$. Upstream, fermiLogKernel_hasDerivAt states the grand-canonical identity $(d/dt)\ln(1+e^{-t})=-\langle n\rangle_F(t)$ for every real $t$, and fermiEnergyKernel_eq_occupation identifies the energy kernel with $t\cdot\langle n\rangle_F$.
Together these encode the textbook relation that mean energy per mode is minus a $\beta$-derivative of $\ln Z$, specialized here to the dimensionless variable $t$.
proof idea
Term-mode, two rewrites then algebra. First apply the derivative clause of fermiLogKernel_hasDerivAt at $t$, so deriv fermiLogKernel t becomes $-\langle n\rangle_F(t)$. The right-hand side $-t\cdot\mathrm{deriv},\mathrm{fermiLogKernel},t$ is therefore $t\cdot\langle n\rangle_F(t)$. Second, rewrite the left-hand side by fermiEnergyKernel_eq_occupation, which equates the energy kernel to $t\cdot\langle n\rangle_F$. The two sides match; ring finishes.
why it matters
Closes item 5 of the module ledger for fermions: pressure and energy kernels are not independent MODEL inputs but derivative-related, exactly as grand-canonical thermodynamics demands. The companion Bose statement appears in the same section under the textbook form $\langle E\rangle=-\partial_\beta\ln Z$ per mode.
In the broader Recognition cosmology stack this legitimates using $t/(e^t+1)$ wherever the $\eta_B$ plasma/radiation chain needs a Fermi energy density built from $\sum e^{-nE/T}$ rather than an ad-hoc kernel. No downstream consumers are wired yet (used_by is empty), so the lemma is presently a local consistency capstone inside StatisticsKernels, parallel to the Bose energy-from-log route and feeding the planned plasmaEnergy_from_occupation style results.
It does not touch the T0–T8 forcing chain, $\phi$-ladder masses, or $\alpha$; it is pure single-mode statistical mechanics supporting the cosmology reduction layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.