IndisputableMonolith.RecogGeom.Quotient

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Indistinguishable
   3
   4/-!
   5# Recognition Geometry: Recognition Quotient
   6
   7This module constructs the recognition quotient C_R = C/~ where ~ is the
   8indistinguishability relation. The quotient collapses configurations that
   9cannot be told apart by the recognizer.
  10
  11## Key Construction
  12
  13Given R : C → E, the recognition quotient is:
  14  C_R = C / ~
  15
  16where c₁ ~ c₂ iff R(c₁) = R(c₂).
  17
  18-/
  19
  20namespace IndisputableMonolith
  21namespace RecogGeom
  22
  23/-! ## Recognition Quotient -/
  24
  25/-- The recognition quotient C_R = C/~ where ~ is indistinguishability. -/
  26def RecognitionQuotient {C E : Type*} (r : Recognizer C E) :=
  27  Quotient (indistinguishableSetoid r)
  28
  29/-- The canonical projection π : C → C_R -/
  30def recognitionQuotientMk {C E : Type*} (r : Recognizer C E) (c : C) :
  31    RecognitionQuotient r :=
  32  Quotient.mk (indistinguishableSetoid r) c
  33
  34/-! ## Quotient Properties -/
  35
  36variable {C E : Type*} (r : Recognizer C E)
  37
  38/-- Two configurations have the same quotient class iff indistinguishable -/
  39theorem quotientMk_eq_iff {c₁ c₂ : C} :
  40    recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ ↔ c₁ ~[r] c₂ :=
  41  Quotient.eq (r := indistinguishableSetoid r)
  42
  43/-- The projection respects the recognizer: same class → same event -/
  44theorem quotientMk_respects_event {c₁ c₂ : C}
  45    (h : recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂) :
  46    r.R c₁ = r.R c₂ :=
  47  (quotientMk_eq_iff r).mp h
  48
  49/-- The quotient is nonempty if C is -/
  50instance [ConfigSpace C] : Nonempty (RecognitionQuotient r) :=
  51  ⟨recognitionQuotientMk r (ConfigSpace.witness C)⟩
  52
  53/-! ## Event Map on Quotient -/
  54
  55/-- The event map factors through the quotient: R = R̄ ∘ π -/
  56def quotientEventMap : RecognitionQuotient r → E :=
  57  Quotient.lift r.R (fun _ _ h => h)
  58
  59/-- The quotient event map makes the diagram commute -/
  60theorem quotientEventMap_spec (c : C) :
  61    quotientEventMap r (recognitionQuotientMk r c) = r.R c := rfl
  62
  63/-- The quotient event map is injective -/
  64theorem quotientEventMap_injective :
  65    Function.Injective (quotientEventMap r) := by
  66  intro q₁ q₂ h
  67  obtain ⟨c₁, hc₁⟩ := Quotient.exists_rep q₁
  68  obtain ⟨c₂, hc₂⟩ := Quotient.exists_rep q₂
  69  simp only [← hc₁, ← hc₂] at h ⊢
  70  -- h : quotientEventMap r ⟦c₁⟧ = quotientEventMap r ⟦c₂⟧
  71  -- which means r.R c₁ = r.R c₂
  72  apply Quotient.sound
  73  exact h
  74
  75/-- The quotient is isomorphic to the image of R -/
  76noncomputable def quotient_equiv_image :
  77    RecognitionQuotient r ≃ Set.range r.R :=
  78  Equiv.ofBijective
  79    (fun q => ⟨quotientEventMap r q,
  80      Quotient.inductionOn q (fun c => ⟨c, rfl⟩)⟩)
  81    ⟨fun q₁ q₂ h => by
  82      simp only [Subtype.mk.injEq] at h
  83      exact quotientEventMap_injective r h,
  84     fun ⟨e, c, hc⟩ => ⟨recognitionQuotientMk r c, by simp [quotientEventMap_spec, hc]⟩⟩
  85
  86/-! ## Lifting Functions to Quotient -/
  87
  88/-- A function f : C → X descends to the quotient if it respects indistinguishability -/
  89def liftToQuotient {X : Type*} (f : C → X)
  90    (hf : ∀ c₁ c₂, Indistinguishable r c₁ c₂ → f c₁ = f c₂) :
  91    RecognitionQuotient r → X :=
  92  Quotient.lift f hf
  93
  94theorem liftToQuotient_spec {X : Type*} (f : C → X)
  95    (hf : ∀ c₁ c₂, Indistinguishable r c₁ c₂ → f c₁ = f c₂) (c : C) :
  96    liftToQuotient r f hf (recognitionQuotientMk r c) = f c := rfl
  97
  98/-! ## Quotient of Local Structure -/
  99
 100/-- The projection of a set U ⊆ C to the quotient -/
 101def projectSet (U : Set C) : Set (RecognitionQuotient r) :=
 102  {q | ∃ c ∈ U, recognitionQuotientMk r c = q}
 103
 104/-- The induced neighborhood structure on the quotient -/
 105def quotientNeighborhoods (L : LocalConfigSpace C) :
 106    RecognitionQuotient r → Set (Set (RecognitionQuotient r)) :=
 107  fun q => {V | ∃ c : C, recognitionQuotientMk r c = q ∧ ∃ U ∈ L.N c, projectSet r U ⊆ V}
 108
 109/-! ## Summary Theorem -/
 110
 111/-- Summary: The recognition quotient captures exactly the observable structure -/
 112theorem recognition_quotient_summary :
 113    Function.Surjective (recognitionQuotientMk r) ∧
 114    Function.Injective (quotientEventMap r) := by
 115  constructor
 116  · intro q
 117    obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 118    exact ⟨c, rfl⟩
 119  · exact quotientEventMap_injective r
 120
 121/-! ## Module Status -/
 122
 123def quotient_status : String :=
 124  "✓ RecognitionQuotient defined (C_R = C/~)\n" ++
 125  "✓ Canonical projection π : C → C_R\n" ++
 126  "✓ quotientMk_eq_iff: same class ↔ indistinguishable\n" ++
 127  "✓ quotientEventMap: R̄ : C_R → E\n" ++
 128  "✓ quotientEventMap_injective: R̄ is injective\n" ++
 129  "✓ quotient_equiv_image: C_R ≃ Im(R)\n" ++
 130  "✓ liftToQuotient: lifting functions\n" ++
 131  "✓ quotientNeighborhoods: induced locality\n" ++
 132  "\n" ++
 133  "RECOGNITION QUOTIENT COMPLETE"
 134
 135#eval quotient_status
 136
 137end RecogGeom
 138end IndisputableMonolith
 139