locally_regular_cell_connected

formal source

  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₂) :
 117    IsRegular L r := by
 118  intro c
 119  obtain ⟨U, hU⟩ := L.N_nonempty c
 120  use U, hU
 121  intro c₁ c₂ _ _
 122  exact hconst c₁ c₂
 123
 124/-! ## The Role of RG5 in Geometry -/
 125
 126/-- **Intuition**: RG5 ensures that "resolution cells don't fragment".
 127
 128    Without RG5, a resolution cell could look like a Cantor set:
 129    infinitely fragmented within any neighborhood. With RG5, resolution
 130    cells are locally "blob-like"—they stay together coherently.
 131