`ehrenfest_theorem`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.ClassicalEmergence on GitHub at line 189.

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

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.