isClassical

formal source

 142  decoherenceTime env > measurementTime
 143
 144/-- A system is in the classical regime if it decoheres before measurement. -/
 145def isClassical (env : EnvironmentCoupling) (measurementTime : ℝ) : Prop :=
 146  decoherenceTime env ≤ measurementTime
 147
 148/-- Quantum and classical are complementary. -/
 149theorem quantum_classical_dichotomy (env : EnvironmentCoupling) (t : ℝ) :
 150    isQuantum env t ∨ isClassical env t := by
 151  unfold isQuantum isClassical
 152  exact le_or_lt (decoherenceTime env) t |>.symm
 153
 154/-! ## Critical Number of Modes -/
 155
 156/-- The critical number of modes at which decoherence equals a given timescale.
 157    Solve: τ_0 × φ^(-N × g) = τ_target
 158    → N = -ln(τ_target/τ_0) / (g × ln(φ)) -/
 159noncomputable def criticalModes (targetTime : ℝ) (coupling : ℝ) : ℝ :=
 160  if coupling > 0 ∧ targetTime > 0 then
 161    -Real.log (targetTime / tau0_seconds) / (coupling * Real.log phi)
 162  else 0
 163
 164/-- The critical modes formula inverts the decoherence formula.
 165    Proof outline: If N = -ln(t/τ₀)/(g·ln(φ)), then:
 166    τ₀ · φ^(-N·g) = τ₀ · φ^(ln(t/τ₀)/ln(φ)) = τ₀ · (t/τ₀) = t -/
 167theorem critical_modes_specification :
 168    ∀ (t g : ℝ), t > 0 → g > 0 →
 169    criticalModes t g = -Real.log (t / tau0_seconds) / (g * Real.log phi) := by
 170  intro t g ht hg
 171  unfold criticalModes
 172  simp [ht, hg]
 173
 174/-! ## Qubit Decoherence Examples -/
 175