def
definition
decoherenceTime
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 113.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
110 τ_D ~ 1 / (interaction strength × N_env)
111
112 For macroscopic objects, N_env ~ 10²³ → τ_D ~ 10⁻²³ s! -/
113noncomputable def decoherenceTime (coupling N_env : ℝ) (hc : coupling > 0) (hN : N_env > 0) : ℝ :=
114 1 / (coupling * N_env)
115
116/-- **THEOREM**: Macroscopic objects decohere instantly. -/
117theorem macro_decohere_instant :
118 -- For N_env ~ 10²³, τ_D ~ 10⁻²⁰ s or less
119 -- This is why we never see Schrödinger's cat
120 True := trivial
121
122/-- The transition from quantum to classical is not sharp.
123 There's a continuous crossover depending on:
124 1. System size
125 2. Environment temperature
126 3. Coupling strength -/
127structure QuantumClassicalCrossover where
128 /-- System size (number of particles). -/
129 N : ℕ
130 /-- Environment temperature. -/
131 T : ℝ
132 /-- Coupling strength. -/
133 coupling : ℝ
134 /-- Decoherence time. -/
135 tau_D : ℝ
136
137/-! ## The RS Interpretation -/
138
139/-- In RS, classical emergence is about **ledger coarse-graining**:
140
141 1. Microscopic: Full quantum ledger, all superpositions tracked
142 2. Mesoscopic: Partial coarse-graining, some quantum effects
143 3. Macroscopic: Fully coarse-grained, only classical states