cell_eq_iff_kernel

formal source

  61
  62/-- Two configurations determine the same cell iff the recognizer cannot
  63distinguish them. -/
  64theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
  65    cellOf I x = cellOf I y ↔ I.kernel x y := by
  66  exact Quotient.eq
  67
  68/-! ## Finite-resolution labels and neighborhoods -/
  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