IndisputableMonolith.RecogGeom.Recognizer

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Core
   3import IndisputableMonolith.RecogGeom.Locality
   4
   5/-!
   6# Recognition Geometry: Recognition Maps (RG2)
   7
   8This module defines recognition maps—the fundamental objects that connect
   9configurations to events. A recognizer is a function R : C → E that maps
  10configurations to observable events.
  11
  12## Axiom RG2: Recognizers and Events
  13
  14There exists at least one recognizer: a map R : C → E for some nontrivial
  15event space E (meaning |Im(R)| ≥ 2).
  16
  17## Key Insight
  18
  19Configurations are what the world does; events are what recognizers see.
  20The recognition map R encodes how the world presents itself to observation.
  21
  22-/
  23
  24namespace IndisputableMonolith
  25namespace RecogGeom
  26
  27/-! ## Recognition Map (RG2) -/
  28
  29/-- A recognition map from configurations to events.
  30    This is the basic object connecting the configuration world
  31    to the observable event world.
  32
  33    RG2: There exists at least one nontrivial recognizer. -/
  34structure Recognizer (C : Type*) (E : Type*) where
  35  /-- The recognition function mapping configurations to events -/
  36  R : C → E
  37  /-- The recognizer is nontrivial: at least two distinct events are produced -/
  38  nontrivial : ∃ c₁ c₂ : C, R c₁ ≠ R c₂
  39
  40/-- A local recognizer is a recognizer on a local configuration space -/
  41structure LocalRecognizer (C : Type*) (E : Type*) extends
  42    LocalConfigSpace C, Recognizer C E
  43
  44/-! ## Basic Properties -/
  45
  46variable {C E : Type*}
  47
  48/-- The image of a recognizer has at least 2 elements -/
  49theorem Recognizer.image_nontrivial (r : Recognizer C E) :
  50    ∃ e₁ e₂ : E, e₁ ∈ Set.range r.R ∧ e₂ ∈ Set.range r.R ∧ e₁ ≠ e₂ := by
  51  obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
  52  exact ⟨r.R c₁, r.R c₂, ⟨c₁, rfl⟩, ⟨c₂, rfl⟩, hne⟩
  53
  54/-- A trivial recognizer maps everything to the same event -/
  55def Recognizer.isTrivial (r : Recognizer C E) : Prop :=
  56  ∀ c₁ c₂ : C, r.R c₁ = r.R c₂
  57
  58/-- No recognizer is trivial (by definition) -/
  59theorem Recognizer.not_trivial (r : Recognizer C E) : ¬r.isTrivial := by
  60  intro h
  61  obtain ⟨c₁, c₂, hne⟩ := r.nontrivial
  62  exact hne (h c₁ c₂)
  63
  64/-! ## Local Image -/
  65
  66/-- The local image of a recognizer on a neighborhood -/
  67def Recognizer.localImage (r : Recognizer C E) (U : Set C) : Set E :=
  68  r.R '' U
  69
  70/-- Local image is subset of full image -/
  71theorem Recognizer.localImage_subset_range (r : Recognizer C E) (U : Set C) :
  72    r.localImage U ⊆ Set.range r.R :=
  73  Set.image_subset_range r.R U
  74
  75/-! ## Preimage Structure -/
  76
  77/-- The preimage (fiber) of an event under a recognizer -/
  78def Recognizer.fiber (r : Recognizer C E) (e : E) : Set C :=
  79  r.R ⁻¹' {e}
  80
  81/-- A configuration is in the fiber of its event -/
  82theorem Recognizer.mem_fiber_self (r : Recognizer C E) (c : C) :
  83    c ∈ r.fiber (r.R c) := by
  84  simp [fiber]
  85
  86/-- Fibers partition the configuration space -/
  87theorem Recognizer.fibers_partition (r : Recognizer C E) :
  88    ∀ c : C, ∃! e : E, c ∈ r.fiber e := by
  89  intro c
  90  use r.R c
  91  constructor
  92  · exact r.mem_fiber_self c
  93  · intro e he
  94    simp [fiber] at he
  95    exact he.symm
  96
  97/-! ## Event Lifting -/
  98
  99/-- An event is realized by some configuration if it's in the image -/
 100def Recognizer.isRealized (r : Recognizer C E) (e : E) : Prop :=
 101  e ∈ Set.range r.R
 102
 103/-- Every event in the image has a witness configuration -/
 104noncomputable def Recognizer.witness (r : Recognizer C E) (e : E)
 105    (he : r.isRealized e) : C :=
 106  he.choose
 107
 108theorem Recognizer.witness_spec (r : Recognizer C E) (e : E)
 109    (he : r.isRealized e) : r.R (r.witness e he) = e :=
 110  he.choose_spec
 111
 112/-! ## Constant Recognizer (Trivial Event Space) -/
 113
 114/-- A constant function is NOT a valid recognizer (it's trivial) -/
 115theorem constant_not_recognizer (C : Type*) [Nonempty C] (e : E) :
 116    ¬∃ c₁ c₂ : C, (fun _ : C => e) c₁ ≠ (fun _ : C => e) c₂ := by
 117  push_neg
 118  intros
 119  rfl
 120
 121/-! ## Module Status -/
 122
 123def recognizer_status : String :=
 124  "✓ Recognizer structure defined (RG2)\n" ++
 125  "✓ LocalRecognizer combining locality and recognition\n" ++
 126  "✓ Nontriviality enforced by definition\n" ++
 127  "✓ Local image and fiber definitions\n" ++
 128  "✓ Fiber partition theorem\n" ++
 129  "✓ Event realization and witness\n" ++
 130  "\n" ++
 131  "RECOGNITION MAPS (RG2) COMPLETE"
 132
 133#eval recognizer_status
 134
 135end RecogGeom
 136end IndisputableMonolith
 137