boseLogKernel_hasDerivAt
plain-language theorem explainer
For a bosonic mode at dimensionless energy t > 0, the derivative of the Bose pressure kernel -ln(1-e^{-t}) equals minus the mean occupation. Workers on the RS plasma and radiation chain cite this to treat pressure and energy kernels as one thermodynamic input. The proof composes elementary real derivatives of exp and log, then rewrites the quotient via the closed form of the Bose occupation.
Claim. For every real $t > 0$, the map $t \mapsto -\ln(1 - e^{-t})$ is differentiable at $t$ with derivative $-\langle n \rangle_B(t)$, where $\langle n \rangle_B(t)$ is the mean occupation of a single bosonic mode at vanishing chemical potential.
background
This module rebuilds the Bose and Fermi statistics kernels from the grand partition function of one mode at $\mu = 0$. Inputs are only the Gibbs weights $e^{-n t}$ and the occupancy sets ($\mathbb{N}$ unrestricted for bosons; ${0,1}$ for fermions), with $t = E/T$ dimensionless.
The Bose pressure kernel is $-\ln(1-e^{-t})$. The mean occupation is the ensemble average $(\sum_n n, w_n)/Z_B$, which evaluates to the Bose–Einstein form $1/(e^t-1)$. Upstream, PhaseSpaceReduction took the pressure and energy kernels as MODEL definitions; here they are recovered from $Z_{\mathrm{mode}} = \sum_n e^{-n t}$.
Grand-canonical thermodynamics demands $\langle n \rangle = -\partial_t \ln Z$. Establishing that identity is the consistency step that makes pressure and energy kernels derivative-related rather than independent inputs.
proof idea
Compose elementary derivatives. Differentiate $s \mapsto -s$, then $s \mapsto e^{-s}$, then $s \mapsto 1 - e^{-s}$. From $t > 0$, the lemma that $e^{-t} < 1$ supplies a nonzero log argument, so the log rule applies; negate to obtain a quotient. Rewrite that quotient by the closed-form occupation identity, using $e^t \neq 0$ and $e^t - 1 \neq 0$ (from $1 < e^t$), then field-simplify and ring to match $-\langle n \rangle_B(t)$.
why it matters
Direct parent of two results in the same module. The first obtains the energy kernel $t/(e^t-1)$ as $-t$ times the derivative of the pressure kernel, so energy is not an independent input. The second is the textbook mode-energy identity $-\partial_\beta \ln Z_B(\beta E) = E,\langle n \rangle_B(\beta E)$.
Together they discharge the module claim that pressure and energy kernels are one thermodynamic object. That closes the grand-canonical consistency step in the derivation chain from $\sum e^{-n E/T}$ up to the plasma pressure and energy capstones on the $\eta_B$ path. Without this derivative link, the earlier MODEL kernels in PhaseSpaceReduction would remain two free functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.