IndisputableMonolith.RecogGeom.Locality

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Core
   3
   4/-!
   5# Recognition Geometry: Locality Structure (RG1)
   6
   7This module defines the neighborhood structure on configuration spaces.
   8Recognition is never global—it is always done from within some finite
   9neighborhood of configurations.
  10
  11## Axiom RG1: Locality / Neighborhoods
  12
  13Each configuration c ∈ C has a family N(c) of neighborhoods satisfying:
  141. Intersection closure: intersections of neighborhoods contain neighborhoods
  152. Refinement: points in a neighborhood have sub-neighborhoods
  16
  17These are the minimal ingredients of a neighborhood structure, allowing us
  18to talk about "varying a configuration a little bit" without committing to
  19a particular topology or metric.
  20
  21-/
  22
  23namespace IndisputableMonolith
  24namespace RecogGeom
  25
  26open Set
  27
  28/-! ## Local Configuration Space (RG1) -/
  29
  30/-- A local configuration space is a configuration space equipped with
  31    a neighborhood structure. This is RG1 of recognition geometry.
  32
  33    The neighborhoods allow us to talk about "nearby" configurations
  34    without assuming a metric or full topology. -/
  35structure LocalConfigSpace (C : Type*) extends ConfigSpace C where
  36  /-- Neighborhood assignment: for each c, a family of "local" sets around c -/
  37  N : C → Set (Set C)
  38
  39  /-- Every neighborhood of c contains c -/
  40  mem_of_mem_N : ∀ c U, U ∈ N c → c ∈ U
  41
  42  /-- Neighborhoods are nonempty for each point -/
  43  N_nonempty : ∀ c, (N c).Nonempty
  44
  45  /-- Intersection closure: if U, V ∈ N(c) both contain c, then there exists
  46      W ∈ N(c) with W ⊆ U ∩ V -/
  47  intersection_closed : ∀ c U V, U ∈ N c → V ∈ N c →
  48    ∃ W ∈ N c, W ⊆ U ∩ V
  49
  50  /-- Refinement: if U ∈ N(c) and c' ∈ U, then there exists V ∈ N(c')
  51      with V ⊆ U -/
  52  refinement : ∀ c U c', U ∈ N c → c' ∈ U →
  53    ∃ V ∈ N c', V ⊆ U
  54
  55/-! ## Basic Lemmas -/
  56
  57variable {C : Type*} (L : LocalConfigSpace C)
  58
  59/-- Every configuration has at least one neighborhood -/
  60theorem LocalConfigSpace.has_neighborhood (c : C) : (L.N c).Nonempty :=
  61  L.N_nonempty c
  62
  63/-- Every point is in its own neighborhoods -/
  64theorem LocalConfigSpace.self_mem_neighborhood (c : C) (U : Set C) (hU : U ∈ L.N c) :
  65    c ∈ U :=
  66  L.mem_of_mem_N c U hU
  67
  68/-- If U and V are neighborhoods of c, there's a common refinement -/
  69theorem LocalConfigSpace.common_refinement (c : C) (U V : Set C)
  70    (hU : U ∈ L.N c) (hV : V ∈ L.N c) :
  71    ∃ W ∈ L.N c, W ⊆ U ∧ W ⊆ V := by
  72  obtain ⟨W, hW, hWUV⟩ := L.intersection_closed c U V hU hV
  73  exact ⟨W, hW, subset_inter_iff.mp hWUV⟩
  74
  75/-- Points in a neighborhood have sub-neighborhoods -/
  76theorem LocalConfigSpace.sub_neighborhood (c c' : C) (U : Set C)
  77    (hU : U ∈ L.N c) (hc' : c' ∈ U) :
  78    ∃ V ∈ L.N c', V ⊆ U :=
  79  L.refinement c U c' hU hc'
  80
  81/-! ## Neighborhood Filter -/
  82
  83/-- The neighborhoods of a point form a filter base -/
  84def LocalConfigSpace.neighborhoodFilterBase (c : C) : FilterBasis C where
  85  sets := L.N c
  86  nonempty := L.N_nonempty c
  87  inter_sets := by
  88    intro U V hU hV
  89    obtain ⟨W, hW, hWsub⟩ := L.intersection_closed c U V hU hV
  90    exact ⟨W, hW, hWsub⟩
  91
  92/-- The neighborhood filter at a point -/
  93noncomputable def LocalConfigSpace.neighborhoodFilter (c : C) : Filter C :=
  94  (L.neighborhoodFilterBase c).filter
  95
  96/-! ## Discrete Configuration Space -/
  97
  98/-- A discrete configuration space where every subset is a neighborhood.
  99    This is the "maximally fine" locality structure. -/
 100def discreteLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
 101  nonempty := inferInstance
 102  N := fun c => {U : Set C | c ∈ U}
 103  mem_of_mem_N := fun c U hU => hU
 104  N_nonempty := fun c => ⟨Set.univ, mem_univ c⟩
 105  intersection_closed := fun c U V hU hV => ⟨U ∩ V, ⟨hU, hV⟩, Subset.rfl⟩
 106  refinement := fun c U c' hU hc' => ⟨U, hc', Subset.rfl⟩
 107
 108/-! ## Trivial Configuration Space -/
 109
 110/-- A trivial configuration space where only the whole space is a neighborhood.
 111    This is the "maximally coarse" locality structure. -/
 112def trivialLocalConfigSpace (C : Type*) [Nonempty C] : LocalConfigSpace C where
 113  nonempty := inferInstance
 114  N := fun _ => {Set.univ}
 115  mem_of_mem_N := fun c U hU => by
 116    simp only [Set.mem_singleton_iff] at hU
 117    rw [hU]
 118    exact mem_univ c
 119  N_nonempty := fun _ => ⟨Set.univ, rfl⟩
 120  intersection_closed := fun _ U V hU hV => by
 121    simp only [Set.mem_singleton_iff] at hU hV
 122    subst hU hV
 123    exact ⟨Set.univ, rfl, Set.inter_self _ ▸ Subset.rfl⟩
 124  refinement := fun _ U _ hU _ => by
 125    simp only [Set.mem_singleton_iff] at hU
 126    exact ⟨Set.univ, rfl, hU ▸ Subset.rfl⟩
 127
 128/-! ## Module Status -/
 129
 130def locality_status : String :=
 131  "✓ LocalConfigSpace defined (RG1)\n" ++
 132  "✓ Neighborhood axioms: mem_of_mem_N, intersection_closed, refinement\n" ++
 133  "✓ Basic lemmas: has_neighborhood, self_mem_neighborhood, common_refinement\n" ++
 134  "✓ Neighborhood filter construction\n" ++
 135  "✓ Discrete and trivial examples\n" ++
 136  "\n" ++
 137  "LOCALITY STRUCTURE (RG1) COMPLETE"
 138
 139#eval locality_status
 140
 141end RecogGeom
 142end IndisputableMonolith
 143