cellLabel

formal source

  69
  70/-- The finite event label of a recognition cell. This is well-defined because
  71the quotient identifies exactly configurations with equal observed labels. -/
  72def cellLabel {K : Type*} (I : PrimitiveInterface K) :
  73    RecognitionLattice I → Fin I.n :=
  74  Quotient.lift (fun x => I.observe x) (by
  75    intro x y h
  76    exact h)
  77
  78@[simp] theorem cellLabel_cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :
  79    cellLabel I (cellOf I x) = I.observe x := rfl
  80
  81/-- A finite-resolution neighborhood: all cells with a given observed label. -/
  82def neighborhood {K : Type*} (I : PrimitiveInterface K) (label : Fin I.n) :
  83    Set (RecognitionLattice I) :=
  84  { c | cellLabel I c = label }
  85
  86/-- The cell of a configuration lies in the neighborhood of its observed label. -/
  87theorem cell_mem_own_neighborhood {K : Type*} (I : PrimitiveInterface K) (x : K) :
  88    cellOf I x ∈ neighborhood I (I.observe x) := by
  89  simp [neighborhood]
  90
  91/-- Every lattice cell has a finite-resolution label. -/
  92theorem every_cell_has_label {K : Type*} (I : PrimitiveInterface K)
  93    (c : RecognitionLattice I) :
  94    ∃ label : Fin I.n, c ∈ neighborhood I label := by
  95  refine ⟨cellLabel I c, ?_⟩
  96  simp [neighborhood]
  97
  98/-! ## Existence from non-trivial recognition -/
  99
 100/-- A non-trivial recognition event forces a recognition lattice. -/
 101theorem nontrivial_recognition_forces_lattice (K : Type*) :
 102    NontrivialRecognition K →