ehrenfest_theorem
plain-language theorem explainer
Ehrenfest's theorem asserts that quantum expectation values obey classical equations of motion, with d⟨x⟩/dt = ⟨p⟩/m and d⟨p⟩/dt = -⟨∂V/∂x⟩ exactly for harmonic potentials and approximately for smooth ones. Researchers modeling quantum-to-classical transitions via many-body J-cost minimization would cite this in derivations of pointer states and decoherence. The proof is a one-line wrapper that applies the trivial tactic to assert the relations hold in the framework.
Claim. $d⟨x⟩/dt = ⟨p⟩/m$ and $d⟨p⟩/dt = -⟨∂V/∂x⟩$, holding exactly for harmonic potentials and approximately for smooth potentials.
background
Recognition Science derives classical emergence from many-body J-cost minimization in module QF-011. Single-particle states allow superpositions at low cost while correlated many-particle states incur J-cost scaling as N² or worse, so product states minimize total cost for large N and yield classical behavior. J-cost is the derived cost of a multiplicative recognizer's comparator on positive ratios, and the cost of any recognition event equals the J-cost of its state.
proof idea
The proof is a one-line wrapper that applies the trivial tactic to assert the Ehrenfest relations hold approximately under the J-cost framework.
why it matters
This places the Ehrenfest theorem inside the classical emergence section of QF-011, linking quantum expectations to the large-N limit of J-cost minimization that selects pointer states. It supports the module's listed predictions on decoherence timescales and classical mechanics as the large-N limit, though no downstream theorems yet apply it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.