IndisputableMonolith.RecogGeom.Symmetry

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Quotient
   3
   4/-!
   5# Recognition Geometry: Symmetries
   6
   7A geometric theory is incomplete without a notion of symmetry. In recognition
   8geometry, symmetry means a transformation of configurations that preserves
   9the recognizable structure.
  10
  11## The Core Idea
  12
  13A transformation T : C → C is a **recognition-preserving map** if:
  141. It preserves events: R(T(c)) = R(c) for all c
  15
  16Such transformations induce well-defined maps on the recognition quotient C_R.
  17Their structure reflects "gauge-like" redundancies that are invisible to
  18the recognizer.
  19
  20## Main Results
  21
  22- `RecognitionPreservingMap`: Definition of symmetry transformations
  23- `symmetry_preserves_indistinguishable`: T preserves indistinguishability
  24- `symmetryQuotientMap`: T induces well-defined map on C_R
  25- Algebraic structure: composition, identity, inverses
  26
  27## Physical Interpretation
  28
  29In physics, gauge symmetries are exactly recognition symmetries: transformations
  30of the underlying state that produce the same observable events. Recognition
  31geometry makes this precise.
  32
  33-/
  34
  35namespace IndisputableMonolith
  36namespace RecogGeom
  37
  38variable {C E : Type*}
  39
  40/-! ## Recognition-Preserving Maps -/
  41
  42/-- A recognition-preserving map is a transformation that preserves events.
  43    This is the fundamental symmetry concept in recognition geometry. -/
  44structure RecognitionPreservingMap (r : Recognizer C E) where
  45  /-- The underlying transformation -/
  46  toFun : C → C
  47  /-- The transformation preserves recognition events -/
  48  preserves_event : ∀ c, r.R (toFun c) = r.R c
  49
  50/-- Coercion to function -/
  51instance (r : Recognizer C E) : CoeFun (RecognitionPreservingMap r) (fun _ => C → C) where
  52  coe := RecognitionPreservingMap.toFun
  53
  54/-! ## Basic Properties -/
  55
  56variable {r : Recognizer C E}
  57
  58/-- A recognition-preserving map preserves indistinguishability -/
  59theorem symmetry_preserves_indistinguishable (T : RecognitionPreservingMap r)
  60    {c₁ c₂ : C} (h : Indistinguishable r c₁ c₂) :
  61    Indistinguishable r (T c₁) (T c₂) := by
  62  unfold Indistinguishable at *
  63  rw [T.preserves_event, T.preserves_event]
  64  exact h
  65
  66/-- A recognition-preserving map preserves distinguishability -/
  67theorem symmetry_preserves_distinguishable (T : RecognitionPreservingMap r)
  68    {c₁ c₂ : C} (h : Distinguishable r c₁ c₂) :
  69    Distinguishable r (T c₁) (T c₂) := by
  70  unfold Distinguishable at *
  71  rw [T.preserves_event, T.preserves_event]
  72  exact h
  73
  74/-- A recognition-preserving map maps resolution cells to resolution cells -/
  75theorem symmetry_maps_cells (T : RecognitionPreservingMap r) (c : C) :
  76    T '' (ResolutionCell r c) ⊆ ResolutionCell r (T c) := by
  77  intro x hx
  78  obtain ⟨c', hc', rfl⟩ := hx
  79  unfold ResolutionCell at *
  80  simp only [Set.mem_setOf_eq] at *
  81  exact symmetry_preserves_indistinguishable T hc'
  82
  83/-! ## Quotient Action -/
  84
  85/-- A recognition-preserving map induces a well-defined map on the quotient -/
  86def symmetryQuotientMap (T : RecognitionPreservingMap r) :
  87    RecognitionQuotient r → RecognitionQuotient r :=
  88  Quotient.lift (fun c => recognitionQuotientMk r (T c)) (fun c₁ c₂ h => by
  89    apply (quotientMk_eq_iff r).mpr
  90    exact symmetry_preserves_indistinguishable T h)
  91
  92theorem symmetryQuotientMap_mk (T : RecognitionPreservingMap r) (c : C) :
  93    symmetryQuotientMap T (recognitionQuotientMk r c) = recognitionQuotientMk r (T c) := rfl
  94
  95/-! ## The Identity Symmetry -/
  96
  97/-- The identity is a recognition-preserving map -/
  98def idSymmetry : RecognitionPreservingMap r where
  99  toFun := id
 100  preserves_event := fun _ => rfl
 101
 102theorem idSymmetry_toFun (c : C) : (idSymmetry (r := r)).toFun c = c := rfl
 103
 104/-- Identity symmetry acts as identity on quotient -/
 105theorem idSymmetry_quotient_action (q : RecognitionQuotient r) :
 106    symmetryQuotientMap idSymmetry q = q := by
 107  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 108  rfl
 109
 110/-! ## Composition of Symmetries -/
 111
 112/-- Composition of recognition-preserving maps -/
 113def compSymmetry (T₁ T₂ : RecognitionPreservingMap r) : RecognitionPreservingMap r where
 114  toFun := T₁.toFun ∘ T₂.toFun
 115  preserves_event := fun c => by
 116    simp only [Function.comp_apply]
 117    rw [T₁.preserves_event, T₂.preserves_event]
 118
 119theorem compSymmetry_toFun (T₁ T₂ : RecognitionPreservingMap r) (c : C) :
 120    (compSymmetry T₁ T₂).toFun c = T₁ (T₂ c) := rfl
 121
 122/-- Composition is associative -/
 123theorem compSymmetry_assoc (T₁ T₂ T₃ : RecognitionPreservingMap r) :
 124    compSymmetry (compSymmetry T₁ T₂) T₃ = compSymmetry T₁ (compSymmetry T₂ T₃) := by
 125  simp only [compSymmetry, Function.comp_assoc]
 126
 127/-- Identity is left neutral -/
 128theorem idSymmetry_comp_left (T : RecognitionPreservingMap r) :
 129    compSymmetry idSymmetry T = T := by
 130  simp only [compSymmetry, idSymmetry, Function.id_comp]
 131
 132/-- Identity is right neutral -/
 133theorem idSymmetry_comp_right (T : RecognitionPreservingMap r) :
 134    compSymmetry T idSymmetry = T := by
 135  simp only [compSymmetry, idSymmetry, Function.comp_id]
 136
 137/-- Composition distributes over quotient action -/
 138theorem compSymmetry_quotient_action (T₁ T₂ : RecognitionPreservingMap r)
 139    (q : RecognitionQuotient r) :
 140    symmetryQuotientMap (compSymmetry T₁ T₂) q =
 141    symmetryQuotientMap T₁ (symmetryQuotientMap T₂ q) := by
 142  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 143  rfl
 144
 145/-! ## Bijective Symmetries (Automorphisms) -/
 146
 147/-- A bijective recognition-preserving map (automorphism) -/
 148structure RecognitionAutomorphism (r : Recognizer C E) extends RecognitionPreservingMap r where
 149  /-- The inverse function -/
 150  invFun : C → C
 151  /-- Left inverse property -/
 152  left_inv : ∀ c, invFun (toFun c) = c
 153  /-- Right inverse property -/
 154  right_inv : ∀ c, toFun (invFun c) = c
 155
 156/-- The inverse of an automorphism preserves events -/
 157theorem RecognitionAutomorphism.inv_preserves_event (T : RecognitionAutomorphism r) (c : C) :
 158    r.R (T.invFun c) = r.R c := by
 159  have h := T.preserves_event (T.invFun c)
 160  rw [T.right_inv] at h
 161  exact h.symm
 162
 163/-- The inverse of an automorphism is an automorphism -/
 164def RecognitionAutomorphism.inv (T : RecognitionAutomorphism r) : RecognitionAutomorphism r where
 165  toFun := T.invFun
 166  preserves_event := T.inv_preserves_event
 167  invFun := T.toFun
 168  left_inv := T.right_inv
 169  right_inv := T.left_inv
 170
 171/-- The identity automorphism -/
 172def idAutomorphism : RecognitionAutomorphism r where
 173  toFun := id
 174  preserves_event := fun _ => rfl
 175  invFun := id
 176  left_inv := fun _ => rfl
 177  right_inv := fun _ => rfl
 178
 179/-- Composition of automorphisms -/
 180def compAutomorphism (T₁ T₂ : RecognitionAutomorphism r) : RecognitionAutomorphism r where
 181  toFun := T₁.toFun ∘ T₂.toFun
 182  preserves_event := fun c => by
 183    simp only [Function.comp_apply]
 184    rw [T₁.preserves_event, T₂.preserves_event]
 185  invFun := T₂.invFun ∘ T₁.invFun
 186  left_inv := fun c => by
 187    simp only [Function.comp_apply]
 188    -- Goal: T₂.invFun (T₁.invFun (T₁.toFun (T₂.toFun c))) = c
 189    have h1 : T₁.invFun (T₁.toFun (T₂.toFun c)) = T₂.toFun c := T₁.left_inv _
 190    rw [h1, T₂.left_inv]
 191  right_inv := fun c => by
 192    simp only [Function.comp_apply]
 193    -- Goal: T₁.toFun (T₂.toFun (T₂.invFun (T₁.invFun c))) = c
 194    have h1 : T₂.toFun (T₂.invFun (T₁.invFun c)) = T₁.invFun c := T₂.right_inv _
 195    rw [h1, T₁.right_inv]
 196
 197/-! ## Algebraic Properties of Automorphisms -/
 198
 199/-- Composition of automorphisms is associative (on toFun) -/
 200theorem compAutomorphism_assoc_toFun (T₁ T₂ T₃ : RecognitionAutomorphism r) :
 201    (compAutomorphism (compAutomorphism T₁ T₂) T₃).toFun =
 202    (compAutomorphism T₁ (compAutomorphism T₂ T₃)).toFun := by
 203  simp only [compAutomorphism, Function.comp_assoc]
 204
 205/-- Identity is left neutral for automorphisms (on toFun) -/
 206theorem idAutomorphism_comp_left_toFun (T : RecognitionAutomorphism r) :
 207    (compAutomorphism idAutomorphism T).toFun = T.toFun := by
 208  simp only [compAutomorphism, idAutomorphism, Function.id_comp]
 209
 210/-- Identity is right neutral for automorphisms (on toFun) -/
 211theorem idAutomorphism_comp_right_toFun (T : RecognitionAutomorphism r) :
 212    (compAutomorphism T idAutomorphism).toFun = T.toFun := by
 213  simp only [compAutomorphism, idAutomorphism, Function.comp_id]
 214
 215/-- Right inverse property (on toFun) -/
 216theorem compAutomorphism_inv_right_toFun (T : RecognitionAutomorphism r) (c : C) :
 217    (compAutomorphism T T.inv).toFun c = c := by
 218  simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
 219  exact T.right_inv c
 220
 221/-- Left inverse property (on toFun) -/
 222theorem compAutomorphism_inv_left_toFun (T : RecognitionAutomorphism r) (c : C) :
 223    (compAutomorphism T.inv T).toFun c = c := by
 224  simp only [compAutomorphism, RecognitionAutomorphism.inv, Function.comp_apply]
 225  exact T.left_inv c
 226
 227/-- The composition T ∘ T⁻¹ acts as identity -/
 228theorem compAutomorphism_inv_right_eq_id (T : RecognitionAutomorphism r) :
 229    (compAutomorphism T T.inv).toFun = id := by
 230  ext c
 231  exact compAutomorphism_inv_right_toFun T c
 232
 233/-- The composition T⁻¹ ∘ T acts as identity -/
 234theorem compAutomorphism_inv_left_eq_id (T : RecognitionAutomorphism r) :
 235    (compAutomorphism T.inv T).toFun = id := by
 236  ext c
 237  exact compAutomorphism_inv_left_toFun T c
 238
 239/-! ## Physical Interpretation: Gauge Equivalence -/
 240
 241/-- Two configurations are **gauge equivalent** if there exists a symmetry
 242    mapping one to the other. This captures the physical notion that
 243    gauge-related configurations are "the same" physically. -/
 244def GaugeEquivalent (r : Recognizer C E) (c₁ c₂ : C) : Prop :=
 245  ∃ T : RecognitionAutomorphism r, T.toFun c₁ = c₂
 246
 247/-- Gauge equivalence implies indistinguishability -/
 248theorem gauge_implies_indistinguishable {c₁ c₂ : C}
 249    (h : GaugeEquivalent r c₁ c₂) : Indistinguishable r c₁ c₂ := by
 250  obtain ⟨T, hT⟩ := h
 251  rw [← hT, Indistinguishable, T.preserves_event]
 252
 253/-- Gauge equivalence is reflexive -/
 254theorem gaugeEquivalent_refl (c : C) : GaugeEquivalent r c c :=
 255  ⟨idAutomorphism, rfl⟩
 256
 257/-- Gauge equivalence is symmetric -/
 258theorem gaugeEquivalent_symm {c₁ c₂ : C} (h : GaugeEquivalent r c₁ c₂) :
 259    GaugeEquivalent r c₂ c₁ := by
 260  obtain ⟨T, hT⟩ := h
 261  use T.inv
 262  simp only [RecognitionAutomorphism.inv]
 263  rw [← hT, T.left_inv]
 264
 265/-- Gauge equivalence is transitive -/
 266theorem gaugeEquivalent_trans {c₁ c₂ c₃ : C}
 267    (h₁ : GaugeEquivalent r c₁ c₂) (h₂ : GaugeEquivalent r c₂ c₃) :
 268    GaugeEquivalent r c₁ c₃ := by
 269  obtain ⟨T₁, hT₁⟩ := h₁
 270  obtain ⟨T₂, hT₂⟩ := h₂
 271  use compAutomorphism T₂ T₁
 272  simp only [compAutomorphism, Function.comp_apply]
 273  rw [hT₁, hT₂]
 274
 275/-! ## Module Status -/
 276
 277def symmetry_status : String :=
 278  "✓ RecognitionPreservingMap defined\n" ++
 279  "✓ symmetry_preserves_indistinguishable proved\n" ++
 280  "✓ symmetryQuotientMap: symmetries induce quotient maps\n" ++
 281  "✓ idSymmetry, compSymmetry with algebraic properties\n" ++
 282  "✓ RecognitionAutomorphism: bijective symmetries\n" ++
 283  "✓ inv, compAutomorphism with group axioms\n" ++
 284  "✓ GaugeEquivalent: physical gauge interpretation\n" ++
 285  "✓ Gauge equivalence is an equivalence relation\n" ++
 286  "\n" ++
 287  "SYMMETRY COMPLETE"
 288
 289#eval symmetry_status
 290
 291end RecogGeom
 292end IndisputableMonolith
 293