finite_resolution_cell_finite_events

formal source

  60
  61/-- If R has finite local resolution at c, the resolution cell at c
  62    has a finite number of "neighbors" in any finite-resolution neighborhood -/
  63theorem finite_resolution_cell_finite_events (c : C)
  64    (h : HasFiniteLocalResolution L r c) :
  65    ∃ U ∈ L.N c, ∀ c' ∈ U, r.R c' ∈ r.R '' U ∧ (r.R '' U).Finite := by
  66  obtain ⟨U, hU, hfin⟩ := h
  67  use U, hU
  68  intro c' hc'
  69  exact ⟨⟨c', hc', rfl⟩, hfin⟩
  70
  71/-! ## Discrete Local Recognition Geometry -/
  72
  73/-- A recognition geometry is locally discrete if events are finite everywhere -/
  74def IsLocallyDiscrete (L : LocalConfigSpace C) (r : Recognizer C E) : Prop :=
  75  HasFiniteResolution L r
  76
  77/-- In a locally discrete recognition geometry, every neighborhood contains
  78    only finitely many distinguishable configurations -/
  79theorem locally_discrete_finite_classes
  80    (h : IsLocallyDiscrete L r) (c : C) :
  81    ∃ U ∈ L.N c, (r.R '' U).Finite :=
  82  h c
  83
  84/-! ## No Continuous Injection Theorem -/
  85
  86/-- **Key Insight**: If a neighborhood has infinite configurations but finite
  87    events, then the recognizer cannot be injective on that neighborhood.
  88
  89    This explains why discrete recognition geometry fundamentally differs
  90    from continuous Euclidean geometry. -/
  91theorem no_injection_on_infinite_finite (c : C)
  92    (U : Set C) (hU : U ∈ L.N c)
  93    (hinf : Set.Infinite U) (hfin : (r.R '' U).Finite) :