pith. machine review for the scientific record. sign in
theorem proved term proof

classical_limit

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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 - μ)))⁻¹ -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.