boseLogKernel_eq_log_partition
plain-language theorem explainer
For t > 0 the Bose pressure kernel −ln(1−e^{−t}) equals ln Z_B(t), the log of the single-mode bosonic grand partition function. Cosmology and statistical-mechanics arguments that previously treated the kernel as a MODEL input can cite this identity to replace it by ln Z. The proof is a two-step rewrite: the geometric-series evaluation of Z_B followed by Real.log_inv.
Claim. For every real $t > 0$, the Bose pressure kernel equals the logarithm of the bosonic single-mode grand partition function: $-\ln(1-e^{-t}) = \ln Z_B(t)$, where $Z_B(t) = \sum_{n\in\mathbb{N}} e^{-n t}$.
background
The StatisticsKernels module rebuilds the Bose/Fermi pressure and energy kernels from the grand partition function of one mode at vanishing chemical potential. The only inputs are the Gibbs weight $e^{-n t}$ with $t = E/T$ and the occupancy sets: unrestricted $n \in \mathbb{N}$ for bosons, and $n \in {0,1}$ for fermions.
Upstream, PhaseSpaceReduction defined the Bose pressure kernel as $-\ln(1-e^{-t})$ by fiat. In this module the bosonic partition is the tsum $Z_B(t) = \sum_n e^{-n t}$, and the geometric-series theorem states that for $t > 0$ one has $Z_B(t) = (1-e^{-t})^{-1}$. The present identity closes the loop: the old kernel is literally $\ln Z_B$.
The same pattern is repeated for fermions ($\ln(1+e^{-t}) = \ln Z_F$) and then differentiated to recover occupation numbers and energy kernels, so pressure and energy cease to be independent MODEL inputs.
proof idea
Term-mode proof in two rewrites. First apply the geometric-series evaluation: $Z_B(t) = (1-e^{-t})^{-1}$ for $t > 0$. Then Real.log_inv turns $\ln((1-e^{-t})^{-1})$ into $-\ln(1-e^{-t})$. The right-hand side is definitionally the Bose pressure kernel, so rfl finishes.
why it matters
This is step 2 of the module ledger: pressure kernels are $\ln Z$, not free definitions. Downstream, mode_energy_bose uses the identity (via $\ln Z_B$) to prove the textbook relation $-\partial_\beta \ln Z_B(\beta E) = E,\langle n\rangle_B(\beta E)$. The capstone plasmaPressure_from_partitionFunction rewrites the $\eta_B$-chain plasma pressure as a phase-space integral of $T,\ln Z_{\mathrm{mode}}(E/T)$, so only Gibbs weights and occupancy sets remain as inputs.
In the broader Recognition Cosmology stack this discharges the MODEL tag on the Bose log kernel inherited from PhaseSpaceReduction and GrandPotential, aligning the radiation sector with ordinary grand-canonical statistical mechanics before those kernels enter entropy and $\eta_B$ calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.