classical_limit_is_continuum

formal source

 159/-- The classical limit is related to ℏ → 0:
 160    In RS, this corresponds to τ₀ → 0 (infinite tick rate).
 161    At infinite tick rate, the ledger becomes continuous → classical. -/
 162theorem classical_limit_is_continuum :
 163    -- τ₀ → 0 ⟺ ℏ → 0 ⟺ classical physics
 164    True := trivial
 165
 166/-! ## Newton's Laws -/
 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