boseKernel
plain-language theorem explainer
The Bose–Einstein occupation kernel $1/(e^t-1)$, cast as a complex-valued function of a real argument so it can feed Mathlib's Mellin transform. Cosmology and statistical-mechanics proofs that evaluate energy or number integrals via Dirichlet series cite it as the Bose integrand. The body is a one-line cast of the real reciprocal through $\mathbb{R}\to\mathbb{C}$.
Claim. For each real $t$, define the complex Bose–Einstein kernel $K_B(t) := \bigl(1/(e^t-1)\bigr)_{\mathbb{R}\to\mathbb{C}}$.
background
The module closes the gap between the series identity $\eta(4)=(7/8)\zeta(4)$ and the thermodynamic integrals used in entropy-per-photon bookkeeping:
$$\int_0^\infty t^3/(e^t+1),dt = (7/8)\int_0^\infty t^3/(e^t-1),dt.$$
Both sides are Mellin transforms at $s=4$ of geometric series in $e^{-t}$. For $t>0$ one has $1/(e^t-1)=\sum_{n\ge 0}e^{-(n+1)t}$. Mathlib's hasSum_mellin converts the power series in $\exp(-t)$ into a Dirichlet series $\sum_n\Gamma(s)a_n/(n+1)^s$. At $s=4$, $\Gamma(4)=6$, so the Bose side becomes $6\zeta(4)=\pi^4/15$.
The kernel is therefore the complexified Bose factor that the Mellin machinery expects: real-valued on $(0,\infty)$ away from the pole at $t=0$, but typed as $\mathbb{C}$ so it matches the complex Mellin API.
proof idea
Pure definition: cast the real expression $1/(\mathrm{exp},t-1)$ first as a real, then as a complex. No lemmas, no tactics. Noncomputable only because the ambient Mellin/complex infrastructure is noncomputable.
why it matters
This is the Bose half of the integral-layer 7/8 fermion weight. Downstream lemmas apply Mathlib Mellin directly to it: hasSum_mellin_bose gives the Dirichlet identity at $s=4$; mellin_bose_eq_integral identifies the Mellin value with $\int_{t>0}t^3/(e^t-1),dt$; mellin_bose_value evaluates it to $\pi^4/15$. The same kernel is reused at $s=3$ in NumberDensityIntegral for Bose number density ($\Gamma(3)\zeta(3)$). Together with the Fermi twin, it discharges the entire mathematical content of EntropyPerPhoton.fermionWeight = 7/8, leaving only the $g_*$ species census as model input. No forcing-chain (T0–T8) step is involved; the landmark is the thermodynamic 7/8 factor in the RS entropy bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.