Cosmology Partition Kernels

The statistical floor

In statistical mechanics, a partition function is the master tally of a system's possible states. For a single mode of a field, one adds up a Boltzmann weight for each allowed occupancy: zero particles, one particle, two, and so on. The sum's logarithm, called the log partition function, feeds directly into pressure, entropy, and the thermal history of the early universe. This work derives those sums from first principles and proves the resulting occupation numbers match the two classic distributions.

The classical results are well known. For bosons, which can share a state without limit, the single-mode grand partition function is the geometric series Z_B = Σ xⁿ = (1 - x)⁻¹ where x = e^(-t) and t is the inverse temperature in natural units. Its logarithm is -log(1 - x). For fermions, the Pauli exclusion principle restricts occupancy to zero or one, so the sum has just two terms: Z_F = 1 + x, with log Z_F = log(1 + x). The mean occupancy follows from the ratio of the weighted sum to the partition function itself: ⟨n⟩ = 1/(e^t - 1) for bosons, the Bose-Einstein distribution, and 1/(e^t + 1) for fermions, the Fermi-Dirac distribution. These are textbook identities, but here they are not assumed; each one is proved as a theorem.

The framework's contribution is to show where the Pauli restriction comes from. In Recognition Science, the framework that derives physical law from a forced cost of recognition, the eight-tick cycle carries an exchange phase: swapping two fermions multiplies the state by -1 at the half-cycle. A doubly occupied antisymmetric state is its own negative, hence zero, which is the standard argument that occupancy cannot exceed one. The framework takes this exchange sign as the physical fork, then treats everything after it as pure mathematics. The two computations differ only in the occupancy range: all natural numbers for bosons, the two-element set {0, 1} for fermions.

The certificate bundles the results: the log kernels used upstream in the pressure and entropy integrals equal the logs of the derived partition functions, and the two occupation numbers are exactly the Bose-Einstein and Fermi-Dirac distributions. The axioms audit to only the base three of the ambient type theory. What this changes is that the statistical floor beneath the cosmology chain is no longer a definitional choice; it is derived from the exchange phase, with the remaining mathematics carrying no free input.

/-- The Bose partition function as a `tsum`: `Z_B(t) = (1 - e^{-t})⁻¹`. -/
theorem bose_partition_tsum (t : ℝ) (ht : 0 < t) :
    (∑' n : ℕ, Real.exp (-t) ^ n) = (1 - Real.exp (-t))⁻¹ :=
  (bose_partition_hasSum t ht).tsum_eq

/-- The Fermi single-mode grand partition function: Pauli restricts occupancy
to `{0, 1}` (see `fermi_exchange_sign`), so the sum is two terms:
`Z_F(t) = 1 + e^{-t}`. -/
theorem fermi_partition_two_state (t : ℝ) :
    (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ)) = 1 + Real.exp (-t) := by
  simp [Fin.sum_univ_two]

/-- **Bose-Einstein occupation number**: the mean occupancy of a bosonic mode
is `⟨n⟩ = (Σ n·xⁿ)/(Σ xⁿ) = 1/(e^t - 1)`. -/
theorem bose_occupation (t : ℝ) (ht : 0 < t) :
    (∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n) / (∑' n : ℕ, Real.exp (-t) ^ n)
      = 1 / (Real.exp t - 1) := by
  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
  have hξlt : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
  have h1 : (1 : ℝ) - Real.exp (-t) ≠ 0 := by linarith
  have hE1 : Real.exp t - 1 ≠ 0 := by
    have h0 : Real.exp 0 < Real.exp t := Real.exp_lt_exp.mpr ht
    rw [Real.exp_zero] at h0
    linarith
  have hprod : Real.exp (-t) * Real.exp t = 1 := by
    rw [← Real.exp_add]
    simp
  rw [(bose_weighted_hasSum t ht).tsum_eq, bose_partition_tsum t ht]
  field_simp
  linear_combination hprod

/-- **Fermi-Dirac occupation number**: the mean occupancy of a fermionic mode
is `⟨n⟩ = (0·1 + 1·x)/(1 + x) = 1/(e^t + 1)`. -/
theorem fermi_occupation (t : ℝ) :
    (∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
        / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
      = 1 / (Real.exp t + 1) := by
  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
  have hEpos : (0 : ℝ) < Real.exp t := Real.exp_pos _
  have h1 : (1 : ℝ) + Real.exp (-t) ≠ 0 := by positivity
  have hE1 : Real.exp t + 1 ≠ 0 := by positivity
  have hprod : Real.exp (-t) * Real.exp t = 1 := by
    rw [← Real.exp_add]
    simp
  simp only [Fin.sum_univ_two]
  norm_num
  field_simp
  linear_combination hprod

/-- `log Z_B` is exactly the Bose log kernel used in
`PhaseSpaceReduction.boseLogKernel` (hence in the pressure/entropy integrals
upstream): the kernel is no longer a definitional choice but the log of the
derived partition function. -/
theorem boseLogKernel_from_partition (t : ℝ) (ht : 0 < t) :
    Real.log (∑' n : ℕ, Real.exp (-t) ^ n)
      = PhaseSpaceReduction.boseLogKernel t := by
  rw [bose_partition_tsum t ht, Real.log_inv,
      PhaseSpaceReduction.boseLogKernel]

/-- `log Z_F` is exactly the Fermi log kernel used in
`PhaseSpaceReduction.fermiLogKernel`. -/
theorem fermiLogKernel_from_partition (t : ℝ) :
    Real.log (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
      = PhaseSpaceReduction.fermiLogKernel t := by
  rw [fermi_partition_two_state, PhaseSpaceReduction.fermiLogKernel]

/-- **RS input (re-export)**: the exchange phase at the half-cycle is `-1`
(fermionic sign), from the eight-tick structure. This is the physical fact
that forces the Pauli occupancy restriction used in the Fermi partition
function below. -/
theorem fermi_exchange_sign :
    Foundation.EightTick.phaseExp ⟨4, by norm_num⟩ = -1 :=
  Foundation.EightTick.spin_statistics_key.1

What this page does not claim

The step from exchange phase -1 to occupancy at most 1 is used as the choice of statement, not derived as a theorem. The framework does not derive the value of the inverse temperature or any specific cosmology timescale.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/PartitionKernels.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: