isRecognitionConnected_subset

formal source

  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,
  93    not scattered fragments. -/
  94structure SatisfiesRG5 (L : LocalConfigSpace C) (r : Recognizer C E) : Prop where
  95  locally_regular : IsRegular L r
  96
  97/-! ## Consequences of Local Regularity -/
  98
  99/-- If a recognizer is locally regular at c, the resolution cell intersected