EnvironmentCoupling

formal source

  80/-! ## Decoherence Time Formula -/
  81
  82/-- The number of environmental modes coupled to the system. -/
  83structure EnvironmentCoupling where
  84  /-- Number of modes. -/
  85  modes : ℕ
  86  /-- Coupling strength (0 to 1). -/
  87  strength : ℝ
  88  strength_bound : 0 ≤ strength ∧ strength ≤ 1
  89
  90/-- Decoherence time for a quantum system with given environment coupling.
  91    τ_decoherence = τ_0 × φ^(-N × g)
  92    where N is number of modes and g is coupling strength. -/
  93noncomputable def decoherenceTime (env : EnvironmentCoupling) : ℝ :=
  94  tau0_seconds * Real.rpow phi (-(env.modes : ℝ) * env.strength)
  95
  96/-- **THEOREM**: Decoherence time decreases with more environmental modes. -/
  97theorem decoherence_decreases_with_modes (env1 env2 : EnvironmentCoupling)
  98    (h : env1.modes < env2.modes) (heq : env1.strength = env2.strength)
  99    (hg : env1.strength > 0) :
 100    decoherenceTime env2 < decoherenceTime env1 := by
 101  unfold decoherenceTime tau0_seconds phi
 102  -- τ₀ × φ^(-n₂g) < τ₀ × φ^(-n₁g) ⟺ φ^(-n₂g) < φ^(-n₁g)
 103  have htau_pos : (7.3e-15 : ℝ) > 0 := by norm_num
 104  rw [heq]
 105  apply mul_lt_mul_of_pos_left _ htau_pos
 106  -- Need: φ^(-n₂g) < φ^(-n₁g), i.e., for φ > 1, -n₂g < -n₁g
 107  have hphi_gt_1 : Constants.phi > 1 := by
 108    have := Constants.phi_gt_onePointFive
 109    linarith
 110  have hg2 : env2.strength > 0 := by rw [← heq]; exact hg
 111  have hexp : -(env2.modes : ℝ) * env2.strength < -(env1.modes : ℝ) * env2.strength := by
 112    have hm : (env1.modes : ℝ) < (env2.modes : ℝ) := Nat.cast_lt.mpr h
 113    nlinarith