IndisputableMonolith.Cosmology.PartitionKernels
Derives Bose and Fermi log-partition kernels and occupation numbers from the per-mode grand partition function, with the fermionic minus sign forced by the eight-tick half-cycle exchange phase. Cosmology workers cite it for the standard factors 1/(e^t∓1) that feed energy integrals. The argument is classical series summation plus a two-state Fermi trace, re-exporting the RS exchange sign.
claimFrom the single-mode grand partition functions $Z_B=\sum_{n=0}^\infty e^{-n t}=1/(1-e^{-t})$ and $Z_F=1+e^{-t}$ (Pauli two-state), the log-kernels are $\log Z_B=-\log(1-e^{-t})$ and $\log Z_F=\log(1+e^{-t})$, and the mean occupations are $n_B=1/(e^{t}-1)$, $n_F=1/(e^{t}+1)$. The Fermi sign $-1$ is the eight-tick half-cycle exchange phase.
background
Recognition Science cosmology builds thermodynamic kernels on the discrete eight-tick clock (Foundation.EightTick): phases $0,\pi/4,\ldots,7\pi/4$. The half-cycle exchange phase is $-1$, which is the physical input that enforces fermionic two-state occupancy rather than an unrestricted sum.
Upstream, PhaseSpaceReduction supplies the $D=3$ reduction of the grand potential to the one-dimensional form $P=(g/2\pi^2),T^4\int t^2 K(t),dt$. The kernel $K$ is not free: it must come from the mode partition function. This module defines those kernels for Bose and Fermi statistics and the associated occupation numbers.
Sibling objects include absolute convergence of the Bose geometric series, the two-state Fermi partition, the log-kernels extracted from $\log Z$, weighted sums for mean occupation, and a certificate packing the main identities.
proof idea
Definition-and-lemma module, not a single theorem. Bose side: geometric series $\sum e^{-nt}$ has sum $1/(1-e^{-t})$ (hasSum/tsum), log-kernel is $-\log(1-e^{-t})$, and the occupation is the weighted sum $\sum n e^{-nt}/Z$, closed as $1/(e^t-1)$. Fermi side: re-export the eight-tick exchange sign $-1$, restrict to the two-state partition $1+e^{-t}$, take $\log Z$, and obtain occupation $1/(e^t+1)$. A certificate aggregates the kernel identities for downstream use.
why it matters in Recognition Science
OccupationEnergy imports this module to connect per-mode occupations to the energy integrands $t^3/(e^t\mp 1)$, whose integrals are already proved ($\pi^4/15$ and $7\pi^4/120$, hence the $7/8$ ratio). Downstream doc-comment: the chain then reads end-to-end from partition function through occupation to the plasma energy/pressure prefactors of PhaseSpaceReduction.
In the RS forcing chain this sits on T7 (eight-tick octave) for the fermionic sign and on T8 ($D=3$) via the upstream phase-space factor. Without these kernels the cosmology pressure/energy formulas remain schematic; with them the Bose/Fermi weights are pinned to standard statistical mechanics forced by the discrete clock rather than postulated.
scope and limits
- Does not evaluate the $t^2$ or $t^3$ momentum integrals; those live in FermionWeightIntegral and related modules.
- Does not derive the $g/(2\pi^2)T^4$ prefactor; that is PhaseSpaceReduction.
- Does not treat interacting gases, chemical potential away from the reduced variable $t$, or non-ideal statistics.
- Does not prove uniqueness of the eight-tick sign; it re-exports that input from Foundation.EightTick.
- Does not address curved spacetime or non-equilibrium distributions.
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