IsLocallyDiscrete

formal source

  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) :
  94    ¬Function.Injective (r.R ∘ Subtype.val : U → E) := by
  95  intro hinj
  96  -- If r.R restricted to U is injective, then U has the same cardinality as r.R '' U
  97  -- But U is infinite and r.R '' U is finite, contradiction
  98  have hUfin : U.Finite := by
  99    apply Set.Finite.of_finite_image hfin
 100    intro x hx y hy hxy
 101    have heq := hinj (a₁ := ⟨x, hx⟩) (a₂ := ⟨y, hy⟩) hxy
 102    simp only [Subtype.mk.injEq] at heq
 103    exact heq
 104  exact hinf hUfin