`classical_limit`

proved

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.PartitionFunction
domain: Thermodynamics
line: 188 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.PartitionFunction on GitHub at line 188.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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
 208/-! ## Implications -/
 209
 210/-- The partition function encodes everything:
 211
 212    1. **Thermodynamic potentials**: F, G, H, S all from Z
 213    2. **Response functions**: C_V, χ from derivatives of Z
 214    3. **Phase transitions**: Singularities in Z
 215    4. **Fluctuations**: ⟨(ΔE)²⟩ from Z -/
 216def implications : List String := [
 217  "Free energy F = -k_B T ln Z",
 218  "Entropy S = -∂F/∂T",

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.