pith. machine review for the scientific record. sign in
structure definition def or abbrev

NeutralWindow

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.