Cosmology Partition Kernels Bose Partition Tsum

The Bose partition sum

In statistical mechanics, a partition function is a sum over all possible states of a system, weighting each state by the Boltzmann factor e^−energy. For a single bosonic mode, the possible occupation numbers are all nonnegative integers: 0, 1, 2, and so on. The declaration bose_partition_tsum proves, in the machine-checked library of formal theorems, that this infinite sum has a simple closed form. Writing x = e^−t with t > 0, the theorem states that Σ_n=0^∞ xⁿ = (1 − x)⁻¹. In terms of the original variable, this is Z_B(t) = (1 − e^−t)⁻¹.

This is the geometric series, a result known since antiquity: the sum 1 + x + x² + x³ + ⋯ converges to 1/(1 − x) whenever |x| < 1. The theorem's content is not the formula itself, but the guarantee that the framework's definition of a bosonic mode, with occupancy ranging over all of ℕ, produces exactly this sum. The proof in the library checks that each term is the Boltzmann weight for occupation number n, that the series converges because 0 < e^−t < 1, and that the limit is the closed form.

The same module derives the mean occupation number ⟨n⟩ = (Σ n·xⁿ)/(Σ xⁿ) = 1/(e^t − 1), the Bose-Einstein distribution. The log of the partition function, log Z_B = −log(1 − e^−t), is shown to equal the framework's boseLogKernel, the quantity used upstream in pressure and entropy integrals for the cosmology thermal history. This means the kernel is not a separate definitional choice; it is the logarithm of a derived partition function.

In Recognition Science, the only physical input that distinguishes this Bose computation from the Fermi one is the allowed occupancy range: all of ℕ for bosons versus {0, 1} for fermions. The fermionic restriction is justified by the exchange sign at the half-cycle of the framework's eight-tick structure, which gives fermions phase −1 under exchange. That step enters as the choice of statement, not as a hidden axiom; everything after it is mathematics with no free input.

What the theorem does not claim: it does not derive the Pauli exclusion principle from first principles, but takes the occupancy restriction as the chosen statement. It does not prove that the physical world contains bosons; it proves a conditional statement about a defined object. And it does not establish the value of any cosmological constant or the actual particle content of the early universe; those remain separate targets.

/-- 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

/-- `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]

/-- **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

What this page does not claim

The theorem does not derive the Pauli exclusion principle from first principles. The theorem does not prove that physical bosons exist. The theorem does not establish any cosmological constant or the particle content of the early universe.

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: