partitionKernelsCert
plain-language theorem explainer
Bundles four equalities: the Bose and Fermi log-pressure kernels equal the logs of the derived per-mode grand partition functions, and the mean occupations equal the Bose–Einstein and Fermi–Dirac distributions. Cosmology thermal-history and phase-space reduction cite it as the statistical-mechanics floor certificate. Proof is a four-tuple packaging of the already-proved component theorems.
Claim. For all $t>0$, $\log\bigl(\sum_{n=0}^\infty e^{-nt}\bigr)$ equals the Bose log-kernel $-\log(1-e^{-t})$; for all real $t$, $\log\bigl(\sum_{n\in\{0,1\}} e^{-nt}\bigr)$ equals the Fermi log-kernel $\log(1+e^{-t})$. Moreover the mean occupations satisfy $\langle n\rangle_B=(\sum n\,e^{-nt})/(\sum e^{-nt})=1/(e^t-1)$ when $t>0$, and $\langle n\rangle_F=1/(e^t+1)$ for all $t$.
background
This module sits under the cosmology thermal-history chain and supplies the per-mode grand partition functions that justify the pressure and entropy kernels used in phase-space reduction. Everything is written in the variable $x=e^{-t}$ with $t>0$, so $0<x<1$ and all geometric series converge.
A bosonic mode has occupancy ranging over $\mathbb{N}$, giving $Z_B=\sum x^n=(1-x)^{-1}$ and $\log Z_B=-\log(1-x)$, which is exactly the Bose pressure kernel defined upstream as $-\log(1-e^{-t})$. A fermionic mode is restricted to occupancy ${0,1}$ (Pauli), so $Z_F=1+x$ and $\log Z_F=\log(1+x)$, matching the Fermi kernel. Mean occupations are the weighted ratios $(\sum n,x^n)/(\sum x^n)$.
The sole physical fork is the occupancy range. The module traces the Fermi restriction to the exchange phase $-1$ at the half-cycle (eight-tick spin-statistics), used only as the choice of index type $\mathrm{Fin},2$; after that fork the derivations are pure analysis.
proof idea
Term-mode four-tuple. The proof is simply
$\langle$boseLogKernel_from_partition, fermiLogKernel_from_partition, bose_occupation, fermi_occupation$\rangle$.
The first component rewrites the Bose tsum as $(1-e^{-t})^{-1}$, takes $\log$ of the inverse, and matches the definition of the Bose log-kernel. The second rewrites the two-state Fermi sum as $1+e^{-t}$ and matches the Fermi log-kernel definition. The third evaluates the weighted geometric series $\sum n,x^n=x/(1-x)^2$ against $Z_B$ to obtain $1/(e^t-1)$. The fourth is the elementary two-term ratio $(0\cdot 1+1\cdot x)/(1+x)=1/(e^t+1)$.
why it matters
Closes the partition-kernel layer of the cosmology stack: the log kernels consumed by phase-space reduction and radiation-entropy integrals are no longer free definitional choices but logs of derived grand partition functions, and the occupation numbers are the classical Bose–Einstein and Fermi–Dirac laws. The doc-comment flags the certificate for the loop axiom audit (#print axioms must show only the base three).
Within Recognition Science the only RS-specific input is the occupancy fork (full $\mathbb{N}$ vs ${0,1}$), justified by the eight-tick exchange sign rather than by an extra axiom. Everything after that fork is standard analysis, so the certificate pins the statistical-mechanics floor beneath the thermal-history chain without introducing new free parameters. No downstream Lean dependents are recorded yet; the intended consumers are the pressure/entropy integrals and the axiom-audit harness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.