boseLogKernel_from_partition
plain-language theorem explainer
For any positive temperature parameter t, the log of the bosonic single-mode grand partition function equals the Bose pressure kernel −log(1−e^{−t}). Cosmology and thermal-history proofs cite this to replace a definitional kernel by the log of a derived geometric series. The proof is a three-step rewrite: geometric tsum, log of inverse, unfold the kernel.
Claim. For every real $t>0$, $\log\bigl(\sum_{n=0}^{\infty} e^{-nt}\bigr) = -\log(1-e^{-t})$. The right-hand side is the Bose log-kernel used in the phase-space pressure and entropy integrals.
background
The module derives the statistical-mechanics floor under the cosmology thermal-history chain: per-mode grand partition functions for a bosonic and a fermionic mode, the log kernels consumed by phase-space reduction, and the mean occupations $\langle n\rangle=1/(e^t\mp 1)$. Everything is written in the variable $x=e^{-t}$ with $t>0$, so $0<x<1$ and every series converges.
For bosons the occupancy runs over all of $\mathbb{N}$, so the single-mode partition function is the geometric series $Z_B=\sum_n x^n=(1-x)^{-1}$. The Bose log-kernel is defined upstream as $-\log(1-e^{-t})$. The companion lemma bose_partition_tsum already identifies the tsum with $(1-e^{-t})^{-1}$. The only physical fork between Bose and Fermi is the occupancy range; the fermionic restriction to ${0,1}$ is justified by the exchange phase $-1$ at the half-cycle of the eight-tick structure, but that input is not used in the present Bose identity.
proof idea
Term-mode rewrite in three steps. First apply bose_partition_tsum to replace $\sum_n e^{-nt}$ by $(1-e^{-t})^{-1}$. Then Real.log_inv turns $\log$ of that inverse into $-\log(1-e^{-t})$. Finally unfold the definition of PhaseSpaceReduction.boseLogKernel, which is exactly that expression. No analytic estimates beyond the already-proved geometric-series identification are required.
why it matters
Closes the gap between a named kernel in the phase-space reduction layer and the log of an explicitly derived partition function: the kernel is no longer a definitional choice. Downstream, partitionKernelsCert bundles this identity with the Fermi twin and the two occupation-number formulas into a single certificate whose axiom audit must show only the base three axioms. That certificate sits under the cosmology thermal-history chain (pressure and entropy integrals that consume the Bose kernel). In the broader RS picture the only physical input at this layer is the Bose/Fermi occupancy fork; the eight-tick exchange sign forces the Fermi side, while the Bose side is pure geometric-series mathematics once occupancy is unrestricted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.