boseLogKernel
plain-language theorem explainer
Defines the Bose logarithmic kernel −ln(1−e^{−t}) as a complex-valued function of a real argument, the form needed by Mellin-transform machinery. Cosmology and statistical-mechanics developments cite it when splitting entropy integrands into energy plus log kernels, and when identifying pressure with log partition functions. The body is a direct cast of the real expression into ℂ.
Claim. For $t \in \mathbb{R}$, the Bose logarithmic kernel is the complex number $-\ln(1-e^{-t})$ obtained by viewing the real value as an element of $\mathbb{C}$.
background
The module derives the radiation identity $s=(4/3)\rho/T$ for a massless quantum gas from the microscopic entropy functional, rather than assuming the thermodynamic factor. Pointwise, the Bose entropy integrand splits as
$$\sigma_B(x)=\frac{x^3}{e^x-1}+x^2\bigl(-\ln(1-e^{-x})\bigr).$$
The second summand is the Bose log kernel. A real-valued twin already appears in phase-space reduction as the Bose pressure kernel $-\ln(1-e^{-t})$. Here the same expression is lifted to $\mathbb{C}$ so that Mellin transforms, summability lemmas, and complex analysis APIs apply without leaving the real line at each step.
Sibling Fermi kernel $\ln(1+e^{-t})$ plays the analogous role for Fermi–Dirac statistics. Downstream partition work shows that $\log Z_B$ equals this kernel, so the definition is not an arbitrary choice but the log of the geometric Bose series.
proof idea
Pure definition: evaluate $-\mathrm{Real.log}(1-e^{-t})$ on $\mathbb{R}$ and coerce the result into $\mathbb{C}$. No lemmas, no tactics; noncomputable only because real logarithm and exponential are.
why it matters
Anchors the log half of the Bose entropy split used to prove $\int\sigma_B=(4/3)\int x^3/(e^x-1)$ and the coefficient $2\pi^2/45$ in $s_\gamma$. Downstream, hasSum_mellin_boseLog and the Mellin-value lemmas treat this kernel as the transform input; boseLogKernel_from_partition and partitionKernelsCert identify it with $\log Z_B$; phase-space reduction feeds it into phaseSpacePressure_closed_form (Stefan–Boltzmann with $7/8$) and phaseSpacePressure_potential ($s=dP/dT$). In the broader $\eta_B$ and radiation chain it supplies the Bose pressure/entropy kernel without smuggling in $4/3$ by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.