Environment

formal source

  53/-! ## The Environment and Decoherence -/
  54
  55/-- An environment model - many degrees of freedom. -/
  56structure Environment where
  57  degrees_of_freedom : ℕ
  58  temperature : ℝ
  59  interaction_strength : ℝ
  60  temp_pos : temperature > 0
  61
  62/-- A typical macroscopic environment (room temperature, many particles). -/
  63def roomEnvironment : Environment := {
  64  degrees_of_freedom := 10^23,
  65  temperature := 300,
  66  interaction_strength := 0.1,
  67  temp_pos := by norm_num
  68}
  69
  70/-! ## Neutral Windows in J-Cost Landscape -/
  71
  72/-- A neutral window is a region where J-cost is locally flat/minimal.
  73
  74    In the configuration space of the system, certain states
  75    have special stability properties. These are the pointer states. -/
  76structure NeutralWindow where
  77  /-- Center of the window (a particular state) -/
  78  center : ℂ
  79  /-- Width of the stable region -/
  80  width : ℝ
  81  /-- J-cost at the center (should be local minimum) -/
  82  cost_at_center : ℝ
  83  /-- Is it a local minimum? -/
  84  is_local_minimum : Bool
  85
  86/-- **THEOREM**: Pointer states occupy neutral windows.