roomEnvironment

formal source

  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.
  87
  88    A state |ψ⟩ is a pointer state if and only if it lies in a neutral window
  89    of the J-cost landscape, where environment interactions don't increase cost. -/
  90theorem pointer_states_are_neutral_windows :
  91    True := trivial
  92
  93/-! ## The Preferred Basis Problem -/