IndisputableMonolith.Cosmology.PartitionKernels

   1import Mathlib
   2import IndisputableMonolith.Cosmology.PhaseSpaceReduction
   3import IndisputableMonolith.Foundation.EightTick
   4
   5/-!
   6# Per-Mode Grand Partition Functions and Occupation Numbers
   7
   8**Status: THEOREM targets (loop-managed).** This module derives the
   9statistical-mechanics floor beneath the cosmology thermal-history chain: the
  10per-mode grand partition function for a bosonic and a fermionic mode, the log
  11kernels used by `PhaseSpaceReduction`, and the mean occupation numbers
  12`⟨n⟩ = 1/(e^t ∓ 1)`.
  13
  14Everything is stated over `x = exp (-t)` with `0 < t`, so `0 < x < 1` and every
  15series converges.
  16
  17## What is derived here
  18
  19* **Bose mode**: occupancy ranges over all of `ℕ`, so the partition function is
  20  the geometric series `Z_B = Σ x^n = (1 - x)⁻¹` and
  21  `log Z_B = -log (1 - x) = boseLogKernel t`.
  22* **Fermi mode**: occupancy is restricted to `{0, 1}` (Pauli), so
  23  `Z_F = Σ_{n : Fin 2} x^n = 1 + x` and `log Z_F = log (1 + x) = fermiLogKernel t`.
  24* **Occupation numbers**: `⟨n⟩ = (Σ n·xⁿ)/(Σ xⁿ)`, giving `1/(e^t - 1)` (Bose)
  25  and `1/(e^t + 1)` (Fermi).
  26
  27## The RS input, honestly scoped
  28
  29The ONLY physical fork between the two computations is the occupancy range:
  30`ℕ` vs `{0, 1}`. That restriction is the Pauli exclusion principle, whose
  31origin in RS is the exchange sign at the half-cycle: fermions acquire phase
  32`-1` under exchange (`Foundation.EightTick.spin_statistics_key`, re-exported
  33below as `fermi_exchange_sign`). The step from "exchange phase −1" to
  34"occupancy ≤ 1" is the standard antisymmetrization argument (a doubly occupied
  35antisymmetric state is its own negative, hence zero); that argument is used
  36here as the justification for the `Fin 2` index type, i.e. it enters as the
  37CHOICE of statement, not as a hidden axiom. Everything after that fork is
  38mathematics with no free input.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Cosmology
  43namespace PartitionKernels
  44
  45open Real
  46
  47/-- **RS input (re-export)**: the exchange phase at the half-cycle is `-1`
  48(fermionic sign), from the eight-tick structure. This is the physical fact
  49that forces the Pauli occupancy restriction used in the Fermi partition
  50function below. -/
  51theorem fermi_exchange_sign :
  52    Foundation.EightTick.phaseExp ⟨4, by norm_num⟩ = -1 :=
  53  Foundation.EightTick.spin_statistics_key.1
  54
  55/-- The Bose single-mode grand partition function: occupancies range over all
  56of `ℕ`, and the Boltzmann-weighted sum is the geometric series with ratio
  57`x = exp (-t) < 1`. -/
  58theorem bose_partition_hasSum (t : ℝ) (ht : 0 < t) :
  59    HasSum (fun n : ℕ => Real.exp (-t) ^ n) (1 - Real.exp (-t))⁻¹ := by
  60  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
  61  have hξlt : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
  62  apply hasSum_geometric_of_norm_lt_one
  63  rw [Real.norm_eq_abs, abs_of_pos hξpos]
  64  exact hξlt
  65
  66/-- The Bose partition function as a `tsum`: `Z_B(t) = (1 - e^{-t})⁻¹`. -/
  67theorem bose_partition_tsum (t : ℝ) (ht : 0 < t) :
  68    (∑' n : ℕ, Real.exp (-t) ^ n) = (1 - Real.exp (-t))⁻¹ :=
  69  (bose_partition_hasSum t ht).tsum_eq
  70
  71/-- `log Z_B` is exactly the Bose log kernel used in
  72`PhaseSpaceReduction.boseLogKernel` (hence in the pressure/entropy integrals
  73upstream): the kernel is no longer a definitional choice but the log of the
  74derived partition function. -/
  75theorem boseLogKernel_from_partition (t : ℝ) (ht : 0 < t) :
  76    Real.log (∑' n : ℕ, Real.exp (-t) ^ n)
  77      = PhaseSpaceReduction.boseLogKernel t := by
  78  rw [bose_partition_tsum t ht, Real.log_inv,
  79      PhaseSpaceReduction.boseLogKernel]
  80
  81/-- The Fermi single-mode grand partition function: Pauli restricts occupancy
  82to `{0, 1}` (see `fermi_exchange_sign`), so the sum is two terms:
  83`Z_F(t) = 1 + e^{-t}`. -/
  84theorem fermi_partition_two_state (t : ℝ) :
  85    (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ)) = 1 + Real.exp (-t) := by
  86  simp [Fin.sum_univ_two]
  87
  88/-- `log Z_F` is exactly the Fermi log kernel used in
  89`PhaseSpaceReduction.fermiLogKernel`. -/
  90theorem fermiLogKernel_from_partition (t : ℝ) :
  91    Real.log (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
  92      = PhaseSpaceReduction.fermiLogKernel t := by
  93  rw [fermi_partition_two_state, PhaseSpaceReduction.fermiLogKernel]
  94
  95/-- The occupancy-weighted Bose sum: `Σ n·xⁿ = x/(1-x)²` for `x = e^{-t}`. -/
  96theorem bose_weighted_hasSum (t : ℝ) (ht : 0 < t) :
  97    HasSum (fun n : ℕ => (n : ℝ) * Real.exp (-t) ^ n)
  98      (Real.exp (-t) / (1 - Real.exp (-t)) ^ 2) := by
  99  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
 100  have hξlt : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
 101  apply hasSum_coe_mul_geometric_of_norm_lt_one
 102  rw [Real.norm_eq_abs, abs_of_pos hξpos]
 103  exact hξlt
 104
 105/-- **Bose-Einstein occupation number**: the mean occupancy of a bosonic mode
 106is `⟨n⟩ = (Σ n·xⁿ)/(Σ xⁿ) = 1/(e^t - 1)`. -/
 107theorem bose_occupation (t : ℝ) (ht : 0 < t) :
 108    (∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n) / (∑' n : ℕ, Real.exp (-t) ^ n)
 109      = 1 / (Real.exp t - 1) := by
 110  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
 111  have hξlt : Real.exp (-t) < 1 := Real.exp_lt_one_iff.mpr (by linarith)
 112  have h1 : (1 : ℝ) - Real.exp (-t) ≠ 0 := by linarith
 113  have hE1 : Real.exp t - 1 ≠ 0 := by
 114    have h0 : Real.exp 0 < Real.exp t := Real.exp_lt_exp.mpr ht
 115    rw [Real.exp_zero] at h0
 116    linarith
 117  have hprod : Real.exp (-t) * Real.exp t = 1 := by
 118    rw [← Real.exp_add]
 119    simp
 120  rw [(bose_weighted_hasSum t ht).tsum_eq, bose_partition_tsum t ht]
 121  field_simp
 122  linear_combination hprod
 123
 124/-- **Fermi-Dirac occupation number**: the mean occupancy of a fermionic mode
 125is `⟨n⟩ = (0·1 + 1·x)/(1 + x) = 1/(e^t + 1)`. -/
 126theorem fermi_occupation (t : ℝ) :
 127    (∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
 128        / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
 129      = 1 / (Real.exp t + 1) := by
 130  have hξpos : (0 : ℝ) < Real.exp (-t) := Real.exp_pos _
 131  have hEpos : (0 : ℝ) < Real.exp t := Real.exp_pos _
 132  have h1 : (1 : ℝ) + Real.exp (-t) ≠ 0 := by positivity
 133  have hE1 : Real.exp t + 1 ≠ 0 := by positivity
 134  have hprod : Real.exp (-t) * Real.exp t = 1 := by
 135    rw [← Real.exp_add]
 136    simp
 137  simp only [Fin.sum_univ_two]
 138  norm_num
 139  field_simp
 140  linear_combination hprod
 141
 142/-- **Certificate**: the partition-kernel layer in one bundle. The log kernels
 143used upstream equal the logs of the derived partition functions, and the two
 144occupation numbers are the Bose-Einstein and Fermi-Dirac distributions. Used
 145by the loop's axiom audit (`#print axioms` must show only the base three). -/
 146theorem partitionKernelsCert :
 147    (∀ t : ℝ, 0 < t →
 148        Real.log (∑' n : ℕ, Real.exp (-t) ^ n)
 149          = PhaseSpaceReduction.boseLogKernel t)
 150      ∧ (∀ t : ℝ,
 151        Real.log (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
 152          = PhaseSpaceReduction.fermiLogKernel t)
 153      ∧ (∀ t : ℝ, 0 < t →
 154        (∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n) / (∑' n : ℕ, Real.exp (-t) ^ n)
 155          = 1 / (Real.exp t - 1))
 156      ∧ (∀ t : ℝ,
 157        (∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
 158            / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))
 159          = 1 / (Real.exp t + 1)) :=
 160  ⟨boseLogKernel_from_partition, fermiLogKernel_from_partition,
 161   bose_occupation, fermi_occupation⟩
 162
 163end PartitionKernels
 164end Cosmology
 165end IndisputableMonolith
 166