IndisputableMonolith.Cosmology.PartitionKernels
Derives Bose and Fermi log-partition kernels and mean occupation numbers from the grand partition function per mode. The fermionic exchange phase −1 is re-exported from the eight-tick half-cycle and forces two-state Pauli occupancy. Cosmology and statistical-mechanics proofs that need n_B(t)=1/(e^t−1) and n_F(t)=1/(e^t+1) cite this module. Arguments are elementary geometric series and two-state traces.
claimFrom the eight-tick half-cycle exchange phase $-1$, the per-mode grand partition functions yield the Bose kernel $\log(1-e^{-t})^{-1}$ and the Fermi kernel $\log(1+e^{-t})$, with mean occupations $n_B(t)=1/(e^t-1)$ and $n_F(t)=1/(e^t+1)$ (Pauli two-state restriction).
background
Recognition Science runs on a discrete eight-tick clock (phases $0,\pi/4,\ldots,7\pi/4$). At the half-cycle the exchange phase is $-1$, the fermionic sign. That single fact is re-exported here and used as the physical input that restricts Fermi modes to occupancy ${0,1}$.
Upstream, Phase-Space Reduction already supplies the three-dimensional prefactor $g/(2\pi^2),T^4$ in the reduced plasma pressure and energy. What remains is the dimensionless kernel $K(t)$ built from the occupation number of a single mode. This module constructs those kernels from the grand partition function: geometric series for bosons, two-state trace for fermions.
Notation: $t=E/T$ is the dimensionless energy; the Bose sum $\sum_{n\ge0}e^{-nt}$ and the Fermi sum $1+e^{-t}$ are the only series that appear.
proof idea
The module is a short derivation chain, not a single theorem. First the eight-tick exchange sign is re-exported as the constant $-1$. Bose side: absolute convergence of $\sum_n e^{-nt}$ for $t>0$ gives the closed form of the partition function, then the log-kernel and the weighted sum that produces $n_B=1/(e^t-1)$. Fermi side: the two-state partition $1+e^{-t}$ (Pauli) yields the log-kernel and $n_F=1/(e^t+1)$ by direct differentiation or ratio of traces. A certificate aggregates the named lemmas. No deep analysis; only geometric-series identities and finite sums.
why it matters in Recognition Science
OccupationEnergy imports this module to connect the occupation numbers $n_B$ and $n_F$ to the energy integrands $t^3/(e^t\mp1)$. Those integrands are already evaluated in FermionWeightIntegral ($\pi^4/15$ and $7\pi^4/120$), giving the classic $7/8$ fermion-to-boson ratio. With PartitionKernels in place the chain runs end-to-end from eight-tick exchange sign through per-mode statistics to the plasma energy density used in RS cosmology.
The module therefore sits between Foundation.EightTick (T7 octave structure) and the thermodynamic observables that inherit $D=3$ from PhaseSpaceReduction (T8). It is the statistical-mechanics hinge of the cosmology stack.
scope and limits
- Does not evaluate the momentum integrals $\int t^2 K(t)\,dt$ or $\int t^3 n(t)\,dt$.
- Does not derive the $g/(2\pi^2)T^4$ prefactor; that lives in PhaseSpaceReduction.
- Does not treat interacting or chemical-potential-dependent gases beyond $\mu=0$ kernels.
- Does not prove uniqueness of the eight-tick sign; it re-exports it as input.
used by (1)
depends on (2)
declarations in this module (10)
-
theorem
fermi_exchange_sign -
theorem
bose_partition_hasSum -
theorem
bose_partition_tsum -
theorem
boseLogKernel_from_partition -
theorem
fermi_partition_two_state -
theorem
fermiLogKernel_from_partition -
theorem
bose_weighted_hasSum -
theorem
bose_occupation -
theorem
fermi_occupation -
theorem
partitionKernelsCert