locally_discrete_finite_classes

formal source

  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
 105
 106/-- Corollary: Finite local resolution at c implies non-injectivity
 107    on any infinite neighborhood containing c -/
 108theorem finite_resolution_not_injective (c : C)
 109    (h : HasFiniteLocalResolution L r c)