Registry · Proposition IV.P27 tau-effective formalized

IV.P27 — Classical Limit

In the limit |m|,|n| → ∞ with mℏ_τ → x and nℏ_τ → p continuous, expectation values satisfy classical equations of motion (Ehrenfest).

Book IV Part 3 Ch. 21

Dependency Graph

Depends on (1)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.Measurement

Symbol: Tau.BookIV.QuantumMechanics.ClassicalLimit