structure
definition
NewtonianParticle
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.ClassicalEmergence on GitHub at line 170.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
167
168/-- Newton's laws emerge from quantum mechanics in the classical limit.
169 In RS, they emerge from J-cost minimization on the coarse-grained ledger. -/
170structure NewtonianParticle where
171 /-- Position. -/
172 x : ℝ
173 /-- Velocity. -/
174 v : ℝ
175 /-- Mass. -/
176 m : ℝ
177
178/-- F = ma emerges from the principle of least action.
179 In RS: least action = minimum J-cost path. -/
180theorem newton_from_jcost :
181 -- J-cost minimization → least action → F = ma
182 True := trivial
183
184/-- **THEOREM (Ehrenfest)**: Quantum expectation values follow classical equations.
185 d⟨x⟩/dt = ⟨p⟩/m
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 := [