boseEnergyKernel_eq_occupation
plain-language theorem explainer
For positive dimensionless ratio t = E/T, the Bose energy kernel equals t times the mean bosonic occupation. Cosmologists wiring plasma energy to the single-mode grand partition function cite this identity. The proof substitutes the Bose–Einstein closed form for occupation and reduces by ring to the explicit kernel t/(e^t−1).
Claim. For every real $t > 0$, the Bose energy kernel equals dimensionless energy times mean bosonic occupation: $\dfrac{t}{e^{t}-1} = t\,\langle n\rangle_B(t)$, where $\langle n\rangle_B(t) = \dfrac{1}{e^{t}-1}$.
background
The Statistics Kernels module rebuilds the Bose and Fermi pressure and energy kernels from the single-mode grand partition function at vanishing chemical potential. Inputs are only the Gibbs weights $e^{-n t}$ with $t = E/T$, and the occupancy sets: unrestricted $n \in \mathbb{N}$ for bosons, and ${0,1}$ for fermions.
PhaseSpaceReduction had introduced the Bose energy kernel as the MODEL formula $t/(e^t-1)$ (occupation times $E/T$). Mean occupation is the ensemble average $(\sum n,w_n)/Z_B$. Upstream, the Bose–Einstein distribution theorem evaluates that average to $1/(e^t-1)$ by dividing the weighted geometric series $\sum n x^n = x/(1-x)^2$ by $Z_B = (1-x)^{-1}$.
This identity is item 4 in the module ledger: energy kernels are $t\cdot\langle n\rangle$, so the plasma-energy integrand is dimensionless energy times mean occupation, not an independent input.
proof idea
Rewrite mean occupation by the Bose–Einstein closed form $1/(e^t-1)$. Unfold the energy kernel to its explicit quotient $t/(e^t-1)$. A single ring step equates the two sides. The hypothesis $t>0$ is inherited from the occupation theorem (geometric series and partition positivity).
why it matters
Two same-module parents consume this identity. The thermodynamic-consistency theorem rewrites the energy kernel as $-t$ times the derivative of the pressure kernel $\ln Z_B$, routing through this equality so pressure in yields energy out with no extra MODEL data. The energy capstone then shows plasma energy equals the phase-space integral of $E\cdot\langle n\rangle(E/T)$ for bosons and fermions, with occupations derived from the same partition functions.
Together these discharge the MODEL status that PhaseSpaceReduction and GrandPotential assigned to the energy kernels, placing the $\eta_B$ plasma chain on $\sum e^{-nE/T}$ footing in momentum space. The Fermi twin is the parallel statement for Pauli occupancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.