boseEnergyKernel_from_logKernel
plain-language theorem explainer
For t>0 the Bose energy kernel equals −t times the derivative of the Bose pressure (log-partition) kernel: t/(e^t−1)=−t·(d/dt)ln Z_B. Anyone deriving plasma energy densities from grand-canonical single-mode sums cites this identity. The proof rewrites via the occupation-as-minus-derivative lemma and the energy-as-t·occupation lemma, then closes by ring algebra.
Claim. For every real $t>0$, the Bose energy kernel equals $-t$ times the derivative of the Bose pressure kernel: $$\frac{t}{e^{t}-1}=-t\cdot\frac{d}{dt}\bigl(-\ln(1-e^{-t})\bigr).$$
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy integrands from a single-mode grand partition function at vanishing chemical potential. The only inputs are the Gibbs weight $e^{-n t}$ with $t=E/T$ and the occupancy sets ($n\in\mathbb{N}$ for bosons). The geometric series yields $Z_B=(1-e^{-t})^{-1}$, so the pressure kernel is literally $\ln Z_B=-\ln(1-e^{-t})$.
Upstream, PhaseSpaceReduction introduced the energy kernel $t/(e^t-1)$ and the log kernel $-\ln(1-e^{-t})$ as bare definitions. Here those objects are recovered from the ensemble: the mean occupation is $\langle n\rangle_B=1/(e^t-1)$, the energy kernel is $t\cdot\langle n\rangle_B$, and grand-canonical consistency demands $\langle n\rangle_B=-d(\ln Z_B)/dt$.
The two supporting lemmas are exactly those facts: boseLogKernel_hasDerivAt states $\mathrm{HasDerivAt},\mathrm{boseLogKernel},(-\langle n\rangle_B),t$, and boseEnergyKernel_eq_occupation states energy kernel $=t\cdot\langle n\rangle_B$.
proof idea
Term-mode proof in two rewrites plus ring. First apply (boseLogKernel_hasDerivAt ht).deriv, which replaces deriv boseLogKernel t by $-\mathrm{boseOccupation},t$. The goal becomes energy kernel $=-t\cdot(-\langle n\rangle_B)=t\cdot\langle n\rangle_B$. Second rewrite with boseEnergyKernel_eq_occupation ht, which replaces the left-hand side by $t\cdot\langle n\rangle_B$. The two sides match; ring discharges the residual arithmetic.
why it matters
Closes step 5 of the module ledger: pressure and energy kernels are not independent MODEL inputs but derivative-related, exactly as the grand-canonical formalism requires. The doc-comment states the slogan directly: "Pressure kernel in, energy kernel out — no independent input."
Together with the occupation and partition identities, this lets the $\eta_B$ plasma energy density start from $\sum e^{-nE/T}$ in momentum space rather than from an ad-hoc energy integrand. No downstream consumers are wired yet (used_by empty), but the Fermi twin and the capstones plasmaEnergy_from_occupation / mode_energy_bose are the natural landing sites. Within Recognition cosmology this is ordinary statistical mechanics scaffolding, not a T0–T8 forcing step; it simply removes a free function from the radiation sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.