IndisputableMonolith.RecogGeom.Indistinguishable

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Recognizer
   3
   4/-!
   5# Recognition Geometry: Indistinguishability (RG3)
   6
   7This module defines the indistinguishability relation induced by a recognizer.
   8Recognition is inherently lossy: multiple configurations may give rise to
   9the same event. The equivalence classes are the "resolution cells"—the
  10smallest units of configuration that can be told apart.
  11
  12## Axiom RG3: Indistinguishability
  13
  14Given a recognition map R : C → E, define an equivalence relation ~ on C by:
  15  c₁ ~ c₂ iff R(c₁) = R(c₂)
  16
  17## Key Insight
  18
  19The equivalence classes of ~ are the "resolution cells" of the recognizer:
  20the smallest units of configuration that can be distinguished by this
  21particular recognition map.
  22
  23-/
  24
  25namespace IndisputableMonolith
  26namespace RecogGeom
  27
  28/-! ## Indistinguishability Relation (RG3) -/
  29
  30/-- Two configurations are indistinguishable under a recognizer if they
  31    produce the same event. This is the fundamental equivalence relation
  32    of recognition geometry. -/
  33def Indistinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
  34  r.R c₁ = r.R c₂
  35
  36/-- Notation: c₁ ~[r] c₂ means c₁ and c₂ are indistinguishable under r -/
  37notation:50 c₁ " ~[" r "] " c₂ => Indistinguishable r c₁ c₂
  38
  39/-! ## Equivalence Relation Properties -/
  40
  41variable {C E : Type*} (r : Recognizer C E)
  42
  43/-- Indistinguishability is reflexive -/
  44theorem Indistinguishable.refl (c : C) : c ~[r] c := rfl
  45
  46/-- Indistinguishability is symmetric -/
  47theorem Indistinguishable.symm' {c₁ c₂ : C} (h : c₁ ~[r] c₂) : c₂ ~[r] c₁ :=
  48  Eq.symm h
  49
  50/-- Indistinguishability is transitive -/
  51theorem Indistinguishable.trans {c₁ c₂ c₃ : C}
  52    (h₁ : c₁ ~[r] c₂) (h₂ : c₂ ~[r] c₃) : c₁ ~[r] c₃ :=
  53  Eq.trans h₁ h₂
  54
  55/-- Indistinguishability is an equivalence relation -/
  56theorem indistinguishable_equivalence : Equivalence (Indistinguishable r) where
  57  refl := Indistinguishable.refl r
  58  symm := Indistinguishable.symm' r
  59  trans := Indistinguishable.trans r
  60
  61/-- The indistinguishability setoid -/
  62def indistinguishableSetoid : Setoid C where
  63  r := Indistinguishable r
  64  iseqv := indistinguishable_equivalence r
  65
  66/-! ## Resolution Cells -/
  67
  68/-- The resolution cell of a configuration c is its equivalence class
  69    under indistinguishability. This is the set of all configurations
  70    that produce the same event as c. -/
  71def ResolutionCell {C E : Type*} (r : Recognizer C E) (c : C) : Set C :=
  72  {c' : C | c' ~[r] c}
  73
  74/-- A configuration is in its own resolution cell -/
  75theorem mem_resolutionCell_self (c : C) : c ∈ ResolutionCell r c :=
  76  Indistinguishable.refl r c
  77
  78/-- Resolution cells are exactly the fibers of the recognizer -/
  79theorem resolutionCell_eq_fiber (c : C) :
  80    ResolutionCell r c = r.fiber (r.R c) := by
  81  ext c'
  82  simp [ResolutionCell, Indistinguishable, Recognizer.fiber]
  83
  84/-- Two configurations have the same resolution cell iff they're indistinguishable -/
  85theorem resolutionCell_eq_iff {c₁ c₂ : C} :
  86    ResolutionCell r c₁ = ResolutionCell r c₂ ↔ c₁ ~[r] c₂ := by
  87  constructor
  88  · intro h
  89    have : c₂ ∈ ResolutionCell r c₁ := by
  90      rw [h]
  91      exact mem_resolutionCell_self r c₂
  92    exact (Indistinguishable.symm' r this)
  93  · intro h
  94    ext c
  95    simp [ResolutionCell, Indistinguishable]
  96    constructor
  97    · intro hc
  98      exact Eq.trans hc h
  99    · intro hc
 100      exact Eq.trans hc (Eq.symm h)
 101
 102/-- Resolution cells partition the configuration space -/
 103theorem resolutionCells_partition (c : C) :
 104    ∃! cell : Set C, c ∈ cell ∧ cell = ResolutionCell r c := by
 105  use ResolutionCell r c
 106  constructor
 107  · exact ⟨mem_resolutionCell_self r c, rfl⟩
 108  · intro cell ⟨_, hcell⟩
 109    exact hcell
 110
 111/-! ## Local Resolution -/
 112
 113/-- The local resolution of R at c on U is the partition of U into
 114    intersections with resolution cells. -/
 115def LocalResolution {C E : Type*} (r : Recognizer C E) (U : Set C) : Set (Set C) :=
 116  {S : Set C | ∃ c ∈ U, S = U ∩ ResolutionCell r c}
 117
 118/-- Local resolution cells cover U -/
 119theorem localResolution_covers (U : Set C) :
 120    ⋃₀ LocalResolution r U = U := by
 121  ext c
 122  simp only [Set.mem_sUnion, LocalResolution, Set.mem_setOf_eq]
 123  constructor
 124  · intro ⟨S, ⟨c', hc'U, hS⟩, hcS⟩
 125    rw [hS] at hcS
 126    exact hcS.1
 127  · intro hcU
 128    refine ⟨U ∩ ResolutionCell r c, ⟨c, hcU, rfl⟩, ?_⟩
 129    exact ⟨hcU, mem_resolutionCell_self r c⟩
 130
 131/-! ## Distinguishability -/
 132
 133/-- Two configurations are distinguishable if they produce different events -/
 134def Distinguishable {C E : Type*} (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
 135  r.R c₁ ≠ r.R c₂
 136
 137/-- Distinguishability is the negation of indistinguishability -/
 138theorem distinguishable_iff_not_indistinguishable {c₁ c₂ : C} :
 139    Distinguishable r c₁ c₂ ↔ ¬(c₁ ~[r] c₂) := Iff.rfl
 140
 141/-- There exist distinguishable configurations (by nontriviality) -/
 142theorem exists_distinguishable :
 143    ∃ c₁ c₂ : C, Distinguishable r c₁ c₂ :=
 144  r.nontrivial
 145
 146/-! ## Module Status -/
 147
 148def indistinguishable_status : String :=
 149  "✓ Indistinguishable relation defined (RG3)\n" ++
 150  "✓ Proved: reflexivity, symmetry, transitivity\n" ++
 151  "✓ Proved: indistinguishable_equivalence\n" ++
 152  "✓ ResolutionCell defined (equivalence classes)\n" ++
 153  "✓ Proved: resolutionCell_eq_fiber\n" ++
 154  "✓ Proved: resolutionCells_partition\n" ++
 155  "✓ LocalResolution defined\n" ++
 156  "✓ Distinguishable defined\n" ++
 157  "\n" ++
 158  "INDISTINGUISHABILITY (RG3) COMPLETE"
 159
 160#eval indistinguishable_status
 161
 162end RecogGeom
 163end IndisputableMonolith
 164