fermiLogKernel_hasDerivAt
plain-language theorem explainer
For every real t, the derivative of the Fermi pressure kernel ln(1+e^{-t}) equals minus the Fermi–Dirac mean occupation. Cosmology and statistical-mechanics proofs cite it to link pressure and energy kernels without independent inputs. The proof is a short calculus chain: differentiate log(1+exp(-s)), then rewrite the quotient as the occupation formula.
Claim. For every real $t$, the map $t \mapsto \ln(1+e^{-t})$ is differentiable at $t$ with derivative $-\langle n\rangle_F(t)$, where $\langle n\rangle_F(t)=1/(e^{t}+1)$ is the Fermi–Dirac mean occupation of a single mode at dimensionless energy $t=E/T$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from a single-mode grand partition function at $\mu=0$, with $t=E/T$. For fermions the occupancy set is ${0,1}$ (Pauli), so $Z_F=1+e^{-t}$. The Fermi pressure kernel is defined as $\ln Z_F$, i.e. $\mathrm{fermiLogKernel}(t)=\ln(1+e^{-t})$, matching the earlier MODEL definition in PhaseSpaceReduction.
Mean occupation is the ensemble average $\langle n\rangle_F=(\sum_{n<2} n,w_n)/Z_F$ with Gibbs weights $w_n=e^{-nt}$. The closed form $\langle n\rangle_F=1/(e^t+1)$ is already proved as fermiOccupation_eq. Grand-canonical thermodynamics then demands $\langle n\rangle=-\partial_t\ln Z$, so the pressure kernel's $t$-derivative must recover minus the occupation; that identity is what this theorem states pointwise via HasDerivAt.
Upstream, the real-valued kernel from PhaseSpaceReduction and the occupation definition in this module are the only analytic ingredients. No Recognition-cost or BIT-kernel structure enters the derivative calculation.
proof idea
Build the derivative of $s\mapsto\ln(1+e^{-s})$ by composition. First, $s\mapsto -s$ has derivative $-1$. Compose with $\exp$ to get derivative $e^{-t}\cdot(-1)$ for $s\mapsto e^{-s}$. Add the constant $1$ to obtain derivative $-e^{-t}$ for $s\mapsto 1+e^{-s}$. Positivity of $1+e^{-t}$ licenses the log rule, yielding derivative $(-e^{-t})/(1+e^{-t})$.
A short algebraic block rewrites that quotient as $-\mathrm{fermiOccupation}(t)$: expand via fermiOccupation_eq, replace $e^{-t}$ by $1/e^{t}$, and clear denominators with field_simp and ring. Rewrite the target derivative and discharge with the log-chain result.
why it matters
This is the Fermi half of the module's thermodynamic-consistency step: pressure and energy kernels are not independent MODEL inputs but derivative-related, as grand-canonical formalism requires. Downstream, fermiEnergyKernel_from_logKernel applies the derivative identity to prove $t/(e^t+1)=-t,(\mathrm{d}/\mathrm{d}t)\ln Z_F$, so the energy kernel is recovered from the log kernel alone. mode_energy_fermi then changes variables to physical $\beta$, obtaining the textbook form $-\partial_\beta\ln Z_F(\beta E)=E\langle n\rangle_F(\beta E)$ by chain rule through this lemma.
In the broader RS cosmology stack, those identities feed the plasma pressure/energy capstones that start from $\sum e^{-nE/T}$ rather than postulated kernels, closing the provenance ledger for the $\eta_B$ radiation sector. No forcing-chain (T0–T8) landmark is touched directly; the result is classical statistical mechanics made machine-checked inside the RS cosmology pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.