cellLabel_cellOf

formal source

  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 →
 103    ∃ (I : PrimitiveInterface K), Nonempty (RecognitionLattice I) := by
 104  intro h
 105  obtain ⟨I, x, _y, _hdist, _hsep⟩ := nontrivial_recognition_forces_interface K h
 106  exact ⟨I, ⟨cellOf I x⟩⟩
 107
 108/-- The minimal two-outcome lattice forced by a distinguished point. -/