IsRegular

formal source

  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
 100    with some neighborhood is still recognition-connected. -/
 101theorem locally_regular_cell_connected (L : LocalConfigSpace C) (r : Recognizer C E)
 102    (c : C) (h : IsLocallyRegular L r c) :
 103    ∃ U ∈ L.N c, IsRecognitionConnected r (ResolutionCell r c ∩ U) := by
 104  obtain ⟨U, hU, hconn⟩ := h
 105  use U, hU
 106  -- ResolutionCell r c = r.R ⁻¹' {r.R c} by definition of Indistinguishable
 107  intro c₁ c₂ h₁ h₂
 108  simp only [ResolutionCell, Set.mem_inter_iff, Set.mem_setOf_eq] at h₁ h₂
 109  -- c₁, c₂ both in preimage of {r.R c} ∩ U
 110  have hc₁ : c₁ ∈ r.R ⁻¹' {r.R c} ∩ U := ⟨h₁.1, h₁.2⟩
 111  have hc₂ : c₂ ∈ r.R ⁻¹' {r.R c} ∩ U := ⟨h₂.1, h₂.2⟩
 112  exact hconn c₁ c₂ hc₁ hc₂
 113
 114/-- A constant recognizer is locally regular everywhere. -/
 115theorem constant_recognizer_regular (L : LocalConfigSpace C) (r : Recognizer C E)
 116    (hconst : ∀ c₁ c₂, r.R c₁ = r.R c₂) :