constant_recognizer_regular

formal source

 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
 132    This is what allows smooth geometric structure to emerge:
 133    resolution cells become the "atoms" of recognition geometry,
 134    and RG5 ensures these atoms are well-behaved. -/
 135
 136/-! ## Module Status -/
 137
 138def connectivity_status : String :=
 139  "✓ IsRecognitionConnected: connected sets defined\n" ++
 140  "✓ isRecognitionConnected_empty: empty set connected\n" ++
 141  "✓ isRecognitionConnected_singleton: singletons connected\n" ++
 142  "✓ isRecognitionConnected_resolutionCell: resolution cells connected\n" ++
 143  "✓ isRecognitionConnected_subset: subsets inherit connectivity\n" ++
 144  "✓ IsLocallyRegular: local regularity at a point (RG5)\n" ++
 145  "✓ IsRegular: global regularity\n" ++