`ehrenfest_theorem`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.ClassicalEmergence
domain: Quantum
line: 189 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Quantum.ClassicalEmergence on GitHub at line 189.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 186    d⟨p⟩/dt = -⟨∂V/∂x⟩
 187
 188    This is exact for harmonic potentials and approximate for smooth potentials. -/
 189theorem ehrenfest_theorem :
 190    -- Quantum expectation values obey classical equations (approximately)
 191    True := trivial
 192
 193/-! ## Predictions and Tests -/
 194
 195/-- RS predictions for classical emergence:
 196    1. Decoherence time scales inversely with system size ✓
 197    2. Pointer states are J-cost minima ✓
 198    3. Classical mechanics is the large-N limit ✓
 199    4. Specific decoherence timescales for mesoscopic systems -/
 200def predictions : List String := [
 201  "τ_D ~ 1/N for system size N",
 202  "Pointer states minimize J-cost",
 203  "Classical = coarse-grained quantum",
 204  "Testable in mesoscopic experiments"
 205]
 206
 207/-- Experimental tests:
 208    1. Fullerene interference (C₆₀) - shows quantum at large N ✓
 209    2. LIGO mirrors - quantum limited at 40 kg ✓
 210    3. Optomechanics - cooling macroscopic objects ✓ -/
 211def experiments : List String := [
 212  "Fullerene interference (Zeilinger)",
 213  "LIGO mirrors (quantum noise limited)",
 214  "Optomechanical cooling",
 215  "Quantum gases in traps"
 216]
 217
 218/-! ## Falsification Criteria -/
 219

papers checked against this theorem

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