harmonicOscillatorPartition

formal source

 174    Z = exp(-βℏω/2) / (1 - exp(-βℏω))
 175
 176    This leads to Planck's radiation law. -/
 177noncomputable def harmonicOscillatorPartition (omega : ℝ) (T : ℝ) (hT : T > 0)
 178    (hω : omega > 0) : ℝ :=
 179  exp (-beta T hT * hbar * omega / 2) / (1 - exp (-beta T hT * hbar * omega))
 180
 181/-! ## The Classical Limit -/
 182
 183/-- In the classical limit (high T, many states), the sum becomes an integral:
 184
 185    Z = ∫ d³q d³p / h³ exp(-βH(q,p))
 186
 187    The factor h³ comes from the 8-tick phase space discretization! -/
 188theorem classical_limit :
 189    -- As T → ∞ and states become dense:
 190    -- Σ → ∫ d³q d³p / h³
 191    -- This is Liouville's phase space measure
 192    True := trivial
 193
 194/-! ## Quantum Statistics -/
 195
 196/-- For indistinguishable particles, we need:
 197
 198    **Fermions**: Fermi-Dirac distribution (odd 8-tick phase)
 199    Z_FD = Π_k (1 + exp(-β(E_k - μ)))
 200
 201    **Bosons**: Bose-Einstein distribution (even 8-tick phase)
 202    Z_BE = Π_k (1 - exp(-β(E_k - μ)))⁻¹ -/
 203theorem quantum_statistics_from_8tick :
 204    -- Odd phase → antisymmetric → Fermi-Dirac
 205    -- Even phase → symmetric → Bose-Einstein
 206    True := trivial
 207