IndisputableMonolith.Cosmology.OccupationEnergy

   1import Mathlib
   2import IndisputableMonolith.Cosmology.PartitionKernels
   3import IndisputableMonolith.Cosmology.FermionWeightIntegral
   4
   5/-!
   6# Energy Kernels from Occupation Numbers
   7
   8**Status: THEOREM targets (loop-managed).** Connects the occupation numbers
   9derived in `PartitionKernels` (from the per-mode grand partition function) to
  10the energy integrands `t³/(e^t ∓ 1)` whose integrals are already proved in
  11`FermionWeightIntegral` (`π⁴/15` and `7π⁴/120`, hence the `7/8` ratio).
  12
  13With this module the chain reads, end to end:
  14
  15  partition function `Z` (PartitionKernels)
  16    → occupation number `⟨n⟩ = 1/(e^t ∓ 1)` (PartitionKernels)
  17    → energy integrand `t³·⟨n⟩` (this module)
  18    → integral values and the `7/8` ratio (FermionWeightIntegral /
  19      ThermalWeightSevenEighths).
  20
  21So `7/8` is derived from the partition function, not merely from a
  22conveniently chosen integrand.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Cosmology
  27namespace OccupationEnergy
  28
  29open Real Set MeasureTheory
  30
  31/-- The Bose energy integrand equals (dimensionless energy per mode `t³`) ×
  32(the occupation number derived from the partition function). -/
  33theorem bose_energy_kernel_eq (t : ℝ) (ht : 0 < t) :
  34    t ^ 3 / (Real.exp t - 1)
  35      = t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
  36          / (∑' n : ℕ, Real.exp (-t) ^ n)) := by
  37  rw [PartitionKernels.bose_occupation t ht]
  38  ring
  39
  40/-- The Fermi energy integrand equals `t³` × (the Pauli-restricted occupation
  41number derived from the two-state partition function). -/
  42theorem fermi_energy_kernel_eq (t : ℝ) (_ht : 0 < t) :
  43    t ^ 3 / (Real.exp t + 1)
  44      = t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
  45          / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))) := by
  46  rw [PartitionKernels.fermi_occupation t]
  47  ring
  48
  49/-- **The 7/8 ratio, stated at the partition-function level**: the ratio of
  50the thermal energy integrals, with each integrand written as
  51`t³ × ⟨n⟩` (occupation numbers from the derived partition functions), is
  52exactly `7/8`. -/
  53theorem energy_ratio_seven_eighths :
  54    (∫ t in Ioi (0 : ℝ),
  55        t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
  56          / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))))
  57      / (∫ t in Ioi (0 : ℝ),
  58        t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
  59          / (∑' n : ℕ, Real.exp (-t) ^ n)))
  60      = 7 / 8 := by
  61  have hf : (∫ t in Ioi (0 : ℝ),
  62      t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
  63        / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))))
  64      = ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t + 1) := by
  65    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
  66    exact (fermi_energy_kernel_eq t ht).symm
  67  have hb : (∫ t in Ioi (0 : ℝ),
  68      t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
  69        / (∑' n : ℕ, Real.exp (-t) ^ n)))
  70      = ∫ t in Ioi (0 : ℝ), t ^ 3 / (Real.exp t - 1) := by
  71    refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
  72    exact (bose_energy_kernel_eq t ht).symm
  73  rw [hf, hb]
  74  exact FermionWeightIntegral.fermi_div_bose_integral
  75
  76/-- **Certificate** for the axiom audit. -/
  77theorem occupationEnergyCert :
  78    (∀ t : ℝ, 0 < t →
  79        t ^ 3 / (Real.exp t - 1)
  80          = t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
  81              / (∑' n : ℕ, Real.exp (-t) ^ n)))
  82      ∧ ((∫ t in Ioi (0 : ℝ),
  83            t ^ 3 * ((∑ n : Fin 2, ((n : ℕ) : ℝ) * Real.exp (-t) ^ (n : ℕ))
  84              / (∑ n : Fin 2, Real.exp (-t) ^ (n : ℕ))))
  85          / (∫ t in Ioi (0 : ℝ),
  86            t ^ 3 * ((∑' n : ℕ, (n : ℝ) * Real.exp (-t) ^ n)
  87              / (∑' n : ℕ, Real.exp (-t) ^ n)))
  88          = 7 / 8) :=
  89  ⟨bose_energy_kernel_eq, energy_ratio_seven_eighths⟩
  90
  91end OccupationEnergy
  92end Cosmology
  93end IndisputableMonolith
  94