IsLocallyRegular

formal source

  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
 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₂