isRecognitionConnected_resolutionCell

formal source

  59  exact Indistinguishable.refl r c
  60
  61/-- A resolution cell is recognition-connected by definition -/
  62theorem isRecognitionConnected_resolutionCell (r : Recognizer C E) (c : C) :
  63    IsRecognitionConnected r (ResolutionCell r c) := by
  64  intro c₁ c₂ h₁ h₂
  65  simp only [ResolutionCell, Set.mem_setOf_eq] at h₁ h₂
  66  exact Indistinguishable.trans r h₁ (Indistinguishable.symm' r h₂)
  67
  68/-- A subset of a recognition-connected set is recognition-connected -/
  69theorem isRecognitionConnected_subset (r : Recognizer C E) {S T : Set C}
  70    (hST : S ⊆ T) (hT : IsRecognitionConnected r T) :
  71    IsRecognitionConnected r S := by
  72  intro c₁ c₂ h₁ h₂
  73  exact hT c₁ c₂ (hST h₁) (hST h₂)
  74
  75/-! ## Local Regularity (RG5) -/
  76
  77/-- A recognizer is locally regular at c if the preimage of r(c) is
  78    recognition-connected within some neighborhood of c.
  79
  80    This means: nearby configurations that produce the same event
  81    are actually "coherently" grouped together. -/
  82def IsLocallyRegular (L : LocalConfigSpace C) (r : Recognizer C E) (c : C) : Prop :=
  83  ∃ U ∈ L.N c, IsRecognitionConnected r (r.R ⁻¹' {r.R c} ∩ U)
  84
  85/-- A recognizer is locally regular everywhere -/
  86def IsRegular (L : LocalConfigSpace C) (r : Recognizer C E) : Prop :=
  87  ∀ c : C, IsLocallyRegular L r c
  88
  89/-- **RG5**: Local Regularity Axiom.
  90
  91    A recognition geometry satisfies RG5 if every recognizer is locally regular.
  92    This ensures that resolution cells form coherent "blobs" within neighborhoods,