boseLogKernel
plain-language theorem explainer
Defines the real Bose pressure kernel K_B(t) = −ln(1−e^{−t}) used in the reduced 1D pressure and energy integrals. Cosmology and statistical-mechanics proofs cite it as the bosonic integrand after angular reduction of the 3D grand-canonical momentum integral. The body is a one-line noncomputable abbreviation of that elementary expression.
Claim. The Bose pressure kernel is the real function $K_B(t) = -\ln(1 - e^{-t})$ for $t \in \mathbb{R}$.
background
The module PhaseSpaceReduction derives the familiar prefactor $g/(2\pi^2),T^4$ in plasma pressure and energy from the underlying 3D momentum-space integral $P = g/(2\pi)^3 \int d^3k, T,K(|k|/T)$, using radial co-area reduction, the unit-ball volume in $\mathbb{R}^3$, and the substitution $k = T t$. The Stefan–Boltzmann exponent 4 is identified as $D+1$ with $D=3$ forced upstream (T8).
In the reduced form one integrates $t^2 K(t),dt$ against a species kernel $K$. For bosons the thermodynamic pressure kernel is the log of the geometric series for the Bose partition function, written here as a real-valued map. A complex sibling of the same formula appears in RadiationEntropyRelation for Mellin-transform work; the present definition is the real version consumed by the phase-space density and closed-form pressure theorems.
proof idea
Pure definition: the body is the elementary expression $-\mathrm{Real.log}(1 - \mathrm{Real.exp}(-t))$. No lemmas or tactics; noncomputable only because real log and exp are.
why it matters
This kernel is the bosonic integrand that turns the abstract 3D phase-space density into concrete radiation thermodynamics. Downstream, plasmaPressure_from_phaseSpace shows that the 3D integral with this kernel (plus the Fermi twin) equals the previously definitional GrandPotential.plasmaPressure; phaseSpacePressure_closed_form then yields the Stefan–Boltzmann law $(\pi^2/90)(g_B+(7/8)g_F)T^4$; and phaseSpacePressure_potential anchors $s=dP/dT$ and the Euler relation at the momentum integral.
PartitionKernels closes the provenance loop: boseLogKernel_from_partition and partitionKernelsCert prove that $\log Z_B(t)$ for $Z_B=(1-e^{-t})^{-1}$ equals this kernel, so the integrand is no longer a modeling choice but the log of the derived Bose partition function. That certificate is part of the axiom-audit surface for the cosmology stack. Framework landmark: the $T^4$ scaling is $D+1$ with $D=3$ from the T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.