finite_resolution_no_chart

formal source

 181    (n : ℕ) :
 182    ¬∃ φ : RecognitionChart L r n, φ.domain = U
 183
 184theorem finite_resolution_no_chart (c : C)
 185    (U : Set C) (hU : U ∈ L.N c)
 186    (hinf : Set.Infinite U) (hfin : (r.R '' U).Finite)
 187    (n : ℕ)
 188    (h : finite_resolution_no_chart_hypothesis (L := L) (r := r) c U hU hinf hfin n) :
 189    ¬∃ φ : RecognitionChart L r n, φ.domain = U :=
 190  h
 191
 192/-- Contrapositive: If a chart exists, either configs are finite or events are infinite -/
 193theorem chart_exists_implies (φ : RecognitionChart L r n)
 194    (c : C) (hc : c ∈ φ.domain)
 195    (h_no_chart : ∀ (c : C) (U : Set C), U ∈ L.N c →
 196      Set.Infinite U → (r.R '' U).Finite → (n : ℕ) →
 197        ¬∃ φ : RecognitionChart L r n, φ.domain = U) :
 198    Set.Finite φ.domain ∨ Set.Infinite (r.R '' φ.domain) := by
 199  by_contra h
 200  push_neg at h
 201  obtain ⟨hinf, hfin⟩ := h
 202  obtain ⟨c', hc'⟩ := φ.domain_is_nbhd
 203  -- Apply finite_resolution_no_chart
 204  exact absurd ⟨φ, rfl⟩ (h_no_chart c' φ.domain hc' hinf hfin n)
 205
 206/-! ## Smooth Structure Emergence -/
 207
 208/-- A recognition geometry is **smooth** if it admits a smooth atlas.
 209
 210    This is the bridge to classical differential geometry: when recognition
 211    structure is "rich enough," the quotient space looks like a manifold. -/
 212def IsSmoothRecognitionGeometry (A : RecognitionAtlas L r n) : Prop :=
 213  -- All transition maps are smooth
 214  -- (This requires additional structure on how charts relate)