boseEnergyKernel
plain-language theorem explainer
The Bose energy kernel is the standard thermal factor t/(e^t−1), i.e. dimensionless energy times mean Bose occupation. Anyone reducing a 3D bosonic phase-space energy integral to a radial 1D form cites it as the integrand. It is a bare closed-form definition, not a derived identity.
Claim. Define the Bose energy kernel by $K_B(t) := \frac{t}{e^{t}-1}$ for $t \in \mathbb{R}$. (Physically this is dimensionless energy times the Bose mean occupation number.)
background
The module PhaseSpaceReduction derives the familiar cosmology prefactor $g/(2\pi^2),T^4$ from a genuine three-dimensional momentum integral, rather than baking the angular factor and $T^4$ scaling into the definition of plasma pressure and energy. Starting from
$P = \frac{g}{(2\pi)^3}\int d^3k, T,K(|k|/T)$,
radial co-area reduction, the unit-ball volume in $\mathbb{R}^3$, and the substitution $k=T t$ produce the reduced form with prefactor $1/(2\pi^2)$ and Stefan–Boltzmann exponent $D+1=4$. Dimension $D=3$ is not an input here; it is forced upstream by T8 in the unified forcing chain.
In that setting the energy density uses an energy kernel in place of the pressure (log-partition) kernel. The Bose energy kernel is the classical factor $t/(e^t-1)$: occupation number times $E/T$. Its Fermi sibling is $t/(e^t+1)$. Both feed the same phase-space density combinator that packages the $g$, $T$, and radial integral.
proof idea
Bare definition: the name is bound to the closed arithmetic expression $t/(\mathrm{exp},t-1)$. No lemmas, no tactics, no integrability side conditions. Downstream theorems unfold this def and rewrite.
why it matters
This kernel is the bosonic energy integrand that lets the module identify the 3D phase-space energy with GrandPotential.plasmaEnergy and then close it to $(\pi^2/30)(g_B+(7/8)g_F)T^4$. Parents: plasmaEnergy_from_phaseSpace (energy from phase space equals the grand-potential energy), phaseSpaceEnergy_closed_form (that closed form), and in StatisticsKernels the identities boseEnergyKernel_eq_occupation ($K_B(t)=t\langle n\rangle_B$), boseEnergyKernel_from_logKernel ($K_B(t)=-t,(\ln Z_B)'$, pressure kernel in, energy kernel out), and the capstone plasmaEnergy_from_occupation. Framework link: the $T^4$ power is $D+1$ with $D=3$ from T8, so the kernel sits on the path from dimension forcing to the radiation energy density used in cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.