mode_energy_bose
plain-language theorem explainer
For a bosonic mode of energy E>0, mean mode energy equals minus the β-derivative of the log partition: −∂_β ln Z_B(βE)=E⟨n⟩_B(βE). Cosmology and statistical-mechanics work that builds radiation energy from single-mode grand partitions cites this identity. The proof composes the Bose log-kernel derivative with argument scaling b↦bE, then rewrites via ln Z = pressure kernel on a neighborhood of β.
Claim. For every mode energy $E>0$ and inverse temperature $\beta>0$, the map $b\mapsto \ln Z_B(bE)$ is differentiable at $\beta$ with derivative $-E\cdot\langle n\rangle_B(\beta E)$, where $Z_B(t)=(1-e^{-t})^{-1}$ is the single-mode Bose partition function and $\langle n\rangle_B(t)=1/(e^t-1)$ is the Bose–Einstein mean occupation.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from the single-mode grand partition at chemical potential zero. The only inputs are Gibbs weights $e^{-n t}$ with $t=E/T$ and the occupancy sets: unrestricted $n\in\mathbb{N}$ for bosons, ${0,1}$ for fermions. The Bose partition is the geometric series $Z_B(t)=(1-e^{-t})^{-1}$; the mean occupation is $\langle n\rangle_B=1/(e^t-1)$.
Earlier modules (PhaseSpaceReduction, GrandPotential) took the pressure kernel $-\ln(1-e^{-t})$ and the energy kernel $t/(e^t-1)$ as model definitions. Here those objects are derived: boseLogKernel_eq_log_partition states that the pressure kernel equals $\ln Z_B(t)$ for $t>0$, and occupation identities recover the Bose–Einstein distribution from the ensemble average.
Thermodynamic consistency then demands that energy and pressure kernels are derivative-related. The local form $\langle n\rangle=-d(\ln Z)/dt$ lifts, after the change of variables $t=\beta E$, to the textbook relation $\langle E\rangle=-\partial_\beta\ln Z$ per mode that this theorem records.
proof idea
Differentiate the scaled argument first: $b\mapsto bE$ has derivative $E$ at $\beta$ (identity times constant). Positivity $\beta E>0$ licenses the upstream derivative of the Bose log-kernel at that point. Chain rule composition yields a derivative for $b\mapsto\mathrm{boseLogKernel}(bE)$; a one-line convert/ring rewrites the chain-rule factor into $-(E\cdot\mathrm{boseOccupation}(\beta E))$.
Finally HasDerivAt.congr_of_eventuallyEq replaces the log-kernel by $\ln(\mathrm{bosePartition}(\cdot))$ on a right neighborhood of $\beta$, using boseLogKernel_eq_log_partition at every $b>0$. The two sides therefore share the same derivative at $\beta$.
why it matters
This is item 5 in the module ledger: thermodynamic consistency of the Bose kernels. Pressure and energy are no longer independent MODEL inputs; once $Z_B$ is fixed by the geometric series, $\langle E\rangle=-\partial_\beta\ln Z$ is forced. That closes the gap between the partition-function derivation and the energy densities used downstream in the $\eta_B$ plasma chain (module capstones plasmaPressure_from_partitionFunction and plasmaEnergy_from_occupation).
In the broader Recognition cosmology stack, radiation and entropy relations import the same Bose log-kernel; having its $\beta$-derivative match $E\langle n\rangle$ means those continuum integrals inherit grand-canonical structure rather than an extra ansatz. No used_by edges are recorded yet for this exact lemma, so it presently sits as a proved interface ready for energy-density and entropy assemblies.
The Fermi twin (stated immediately below in the file) plays the same role for Pauli modes. Together they underwrite the claim that RS radiation thermodynamics starts from $\sum_n e^{-nE/T}$ in momentum space, not from hand-set kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.