Cosmology Partition Kernels Fermi Log Kernel From Partition

The Fermi log kernel

The Fermi-Dirac distribution describes how particles that obey the Pauli exclusion principle, meaning no two can occupy the same quantum state, spread across energy levels. The average number of such particles in a state with energy cost t is 1/(e^t + 1). This is a standard result of statistical mechanics, taught in every thermal physics course, and it follows from a deceptively simple starting point: a single fermionic mode can hold either zero particles or one particle, never more.

That two-option rule is all the physics needed. The grand partition function for one fermionic mode is the sum over its two allowed occupancies, weighted by the Boltzmann factor e^(-t) for one particle: Z = 1 + e^(-t). Its logarithm, log(1 + e^(-t)), is what the framework calls the Fermi log kernel. The declaration fermiLogKernel_from_partition proves, as a theorem in a machine-checked library of formal theorems, that the logarithm of this two-term partition function equals the Fermi log kernel used elsewhere in the framework's cosmology chain. The proof is a direct rewrite: the sum evaluates to 1 + e^(-t), and the logarithm of that expression is, by definition, the kernel.

The statement carries no hidden assumptions about the framework's deeper structure. It requires only that t be a real number, with no positivity condition even needed for the Fermi case, since the two-term sum converges for any real t. The theorem does not derive the Pauli principle itself. The framework's input is the exchange sign: within its eight-tick structure, fermions acquire a phase of -1 under exchange, and the standard antisymmetrization argument then forces the occupancy to be at most one. That step enters as the choice of the two-element index set, not as a derived conclusion of this theorem.

What the declaration establishes is a clean equivalence: the log kernel that appears in the framework's pressure and entropy integrals is not a separate definitional choice but the logarithm of a derived partition function. The same bundle of theorems proves the Bose counterpart, where occupancies range over all natural numbers, giving log Z = -log(1 - e^(-t)), and derives the mean occupation numbers 1/(e^t - 1) and 1/(e^t + 1). The Fermi log kernel theorem is the fermionic half of that certificate, grounding one piece of the thermal-history chain in a two-term sum that any undergraduate can verify by hand.

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

/-- 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 theorem does not derive the Pauli exclusion principle itself, it takes the occupancy restriction as a choice of statement. The theorem does not prove the Bose-Einstein or Fermi-Dirac distributions apply to real particles, it only derives the mathematical expressions from the partition functions. The theorem does not establish any physical prediction about the early universe; it is a mathematical identity within the framework's library.

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: