Cosmology Partition Kernels Fermi Partition Two State

The two-state sum

In statistical mechanics, a partition function is a sum over all the states a system can occupy, weighting each by its probability. For a single mode that can hold any number of particles, the sum runs over all natural numbers. For a fermion, the Pauli exclusion principle limits each mode to either zero or one particle. The declaration fermi_partition_two_state proves that this restricted sum is exactly 1 + e^-t, where t is the energy divided by temperature.

The proof is a two-line calculation. The sum over the finite set {0, 1} of e^-t to the power n evaluates to 1 + e^-t. This is not an approximation or a model choice; it is a theorem in the machine-checked library of formal theorems. The same library derives the Fermi-Dirac occupation number 1/(e^t + 1) from this sum, matching the standard result of quantum statistics.

In Recognition Science, the Pauli restriction is not assumed as a separate physical postulate. The framework derives the fermionic exchange sign of -1 from its eight-tick cycle structure. The step from that sign to the occupancy limit is the standard antisymmetrization argument: a doubly occupied antisymmetric state equals its own negative, hence vanishes. This argument enters as the choice of statement, not as a hidden axiom.

The declaration itself does not claim that the Pauli principle is derived from first principles. It takes the two-state restriction as the starting point and proves the sum that follows. The framework's contribution is the exchange sign that motivates the restriction, not the restriction itself. What the theorem establishes is the clean arithmetic of the Fermi partition function once the occupancy range is fixed.

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

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

/-- **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 declaration does not prove the Pauli exclusion principle from more basic principles. The declaration does not establish the physical origin of the two-state occupancy restriction. The declaration does not claim that the Fermi-Dirac distribution applies to interacting systems.

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: