IndisputableMonolith.RecogGeom.Composition

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Quotient
   3
   4/-!
   5# Recognition Geometry: Composition of Recognizers (RG6)
   6
   7Physical measurement does not happen in isolation. Multiple recognizers can act
   8on the same configuration space. This module develops the theory of composite
   9recognizers and proves the fundamental **Refinement Theorem**.
  10
  11## The Key Insight
  12
  13When we combine two recognizers R₁ and R₂, we get a composite recognizer R₁₂
  14that can distinguish configurations that either R₁ or R₂ can distinguish.
  15This means:
  16- The indistinguishability relation becomes finer
  17- The recognition quotient becomes larger (more classes)
  18- We see "more" of the configuration space
  19
  20This is how richer geometry emerges from simpler measurements.
  21
  22## Main Results
  23
  24- `CompositeRecognizer`: The product recognizer R₁₂(c) = (R₁(c), R₂(c))
  25- `composite_refines`: R₁₂ distinguishes at least as much as R₁ or R₂
  26- `composite_indistinguishable_iff`: c₁ ~₁₂ c₂ ↔ (c₁ ~₁ c₂) ∧ (c₁ ~₂ c₂)
  27- `refinement_theorem`: Composite quotient refines both component quotients
  28
  29-/
  30
  31namespace IndisputableMonolith
  32namespace RecogGeom
  33
  34variable {C E₁ E₂ : Type*}
  35
  36/-! ## Composite Recognizer Definition -/
  37
  38/-- The composite of two recognizers produces events in the product space.
  39    This is RG6: composition of recognizers. -/
  40def CompositeRecognizer (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  41    Recognizer C (E₁ × E₂) where
  42  R := fun c => (r₁.R c, r₂.R c)
  43  nontrivial := by
  44    -- Use nontriviality of r₁ to construct distinct events
  45    obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
  46    use c₁, c₂
  47    intro heq
  48    apply hne
  49    exact (Prod.mk.injEq _ _ _ _).mp heq |>.1
  50
  51/-- Notation for composite recognizer -/
  52infixl:70 " ⊗ " => CompositeRecognizer
  53
  54/-! ## Refinement Properties -/
  55
  56/-- The composite recognizer's map is the product of component maps -/
  57theorem composite_R_eq (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
  58    (r₁ ⊗ r₂).R c = (r₁.R c, r₂.R c) := rfl
  59
  60/-- Indistinguishability under composite iff indistinguishable under both -/
  61theorem composite_indistinguishable_iff (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  62    (c₁ c₂ : C) :
  63    Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔
  64    Indistinguishable r₁ c₁ c₂ ∧ Indistinguishable r₂ c₁ c₂ := by
  65  simp only [Indistinguishable, composite_R_eq, Prod.mk.injEq]
  66
  67/-- If configs are indistinguishable under composite, they are under r₁ -/
  68theorem composite_refines_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  69    {c₁ c₂ : C} (h : Indistinguishable (r₁ ⊗ r₂) c₁ c₂) :
  70    Indistinguishable r₁ c₁ c₂ :=
  71  ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).1
  72
  73/-- If configs are indistinguishable under composite, they are under r₂ -/
  74theorem composite_refines_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  75    {c₁ c₂ : C} (h : Indistinguishable (r₁ ⊗ r₂) c₁ c₂) :
  76    Indistinguishable r₂ c₁ c₂ :=
  77  ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).2
  78
  79/-- The composite distinguishes configs that either component distinguishes -/
  80theorem composite_distinguishes (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
  81    {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂ ∨ Distinguishable r₂ c₁ c₂) :
  82    Distinguishable (r₁ ⊗ r₂) c₁ c₂ := by
  83  unfold Distinguishable at *
  84  intro heq
  85  rw [composite_R_eq] at heq
  86  have ⟨h1, h2⟩ := (Prod.mk.injEq _ _ _ _).mp heq
  87  cases h with
  88  | inl h₁ => exact h₁ h1
  89  | inr h₂ => exact h₂ h2
  90
  91/-! ## Resolution Cell Refinement -/
  92
  93/-- Resolution cells under composite are intersections of component cells -/
  94theorem composite_resolutionCell (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
  95    ResolutionCell (r₁ ⊗ r₂) c = ResolutionCell r₁ c ∩ ResolutionCell r₂ c := by
  96  ext c'
  97  simp only [ResolutionCell, Set.mem_setOf_eq, Set.mem_inter_iff,
  98             composite_indistinguishable_iff]
  99
 100/-- Composite resolution cells are subsets of either component cell -/
 101theorem composite_cell_subset_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 102    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₁ c := by
 103  rw [composite_resolutionCell]
 104  exact Set.inter_subset_left
 105
 106theorem composite_cell_subset_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 107    ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₂ c := by
 108  rw [composite_resolutionCell]
 109  exact Set.inter_subset_right
 110
 111/-! ## Quotient Maps -/
 112
 113/-- There is a natural map from the composite quotient to the r₁ quotient -/
 114def quotientMapLeft (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 115    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₁ :=
 116  Quotient.lift (recognitionQuotientMk r₁) (fun c₁ c₂ h =>
 117    (quotientMk_eq_iff r₁).mpr (composite_refines_left r₁ r₂ h))
 118
 119/-- There is a natural map from the composite quotient to the r₂ quotient -/
 120def quotientMapRight (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 121    RecognitionQuotient (r₁ ⊗ r₂) → RecognitionQuotient r₂ :=
 122  Quotient.lift (recognitionQuotientMk r₂) (fun c₁ c₂ h =>
 123    (quotientMk_eq_iff r₂).mpr (composite_refines_right r₁ r₂ h))
 124
 125/-- The quotient maps are surjective -/
 126theorem quotientMapLeft_surjective (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 127    Function.Surjective (quotientMapLeft r₁ r₂) := by
 128  intro q
 129  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 130  use recognitionQuotientMk (r₁ ⊗ r₂) c
 131  rfl
 132
 133theorem quotientMapRight_surjective (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 134    Function.Surjective (quotientMapRight r₁ r₂) := by
 135  intro q
 136  obtain ⟨c, rfl⟩ := Quotient.exists_rep q
 137  use recognitionQuotientMk (r₁ ⊗ r₂) c
 138  rfl
 139
 140/-! ## The Refinement Theorem -/
 141
 142/-- **Refinement Theorem**: The composite quotient refines both component quotients.
 143
 144    This is the fundamental theorem of recognition composition. It says that
 145    combining recognizers gives us a "finer" view of configuration space.
 146    The composite quotient C_{R₁₂} maps onto both C_{R₁} and C_{R₂}.
 147
 148    Mathematically: there exist surjective maps
 149      π₁ : C_{R₁₂} → C_{R₁}
 150      π₂ : C_{R₁₂} → C_{R₂}
 151
 152    This means the composite recognizer "sees" at least as much structure as
 153    either component recognizer. -/
 154theorem refinement_theorem (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 155    Function.Surjective (quotientMapLeft r₁ r₂) ∧
 156    Function.Surjective (quotientMapRight r₁ r₂) :=
 157  ⟨quotientMapLeft_surjective r₁ r₂, quotientMapRight_surjective r₁ r₂⟩
 158
 159/-! ## Associativity and Commutativity -/
 160
 161/-- Composition is commutative up to isomorphism on events -/
 162theorem composite_comm_events (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
 163    (r₁ ⊗ r₂).R c = Prod.swap ((r₂ ⊗ r₁).R c) := by
 164  simp [composite_R_eq]
 165
 166/-- Indistinguishability is symmetric under swap -/
 167theorem composite_comm_indistinguishable (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 168    (c₁ c₂ : C) :
 169    Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔ Indistinguishable (r₂ ⊗ r₁) c₁ c₂ := by
 170  rw [composite_indistinguishable_iff, composite_indistinguishable_iff]
 171  exact And.comm
 172
 173/-! ## N-ary Composition -/
 174
 175/-- Triple composite recognizer -/
 176def CompositeRecognizer₃ {E₃ : Type*}
 177    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃) :
 178    Recognizer C (E₁ × E₂ × E₃) where
 179  R := fun c => (r₁.R c, r₂.R c, r₃.R c)
 180  nontrivial := by
 181    obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
 182    use c₁, c₂
 183    intro heq
 184    apply hne
 185    simp only [Prod.mk.injEq] at heq
 186    exact heq.1
 187
 188/-! ## Information Content -/
 189
 190/-- The composite recognizer has at least as much information as either component.
 191    "Information" here means the ability to distinguish configurations. -/
 192theorem composite_info_monotone_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 193    {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂) :
 194    Distinguishable (r₁ ⊗ r₂) c₁ c₂ :=
 195  composite_distinguishes r₁ r₂ (Or.inl h)
 196
 197theorem composite_info_monotone_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 198    {c₁ c₂ : C} (h : Distinguishable r₂ c₁ c₂) :
 199    Distinguishable (r₁ ⊗ r₂) c₁ c₂ :=
 200  composite_distinguishes r₁ r₂ (Or.inr h)
 201
 202/-! ## Module Status -/
 203
 204def composition_status : String :=
 205  "✓ CompositeRecognizer defined (RG6)\n" ++
 206  "✓ composite_indistinguishable_iff: c₁ ~₁₂ c₂ ↔ (c₁ ~₁ c₂) ∧ (c₁ ~₂ c₂)\n" ++
 207  "✓ composite_refines_left/right: composite refines both components\n" ++
 208  "✓ composite_resolutionCell: cells are intersections\n" ++
 209  "✓ quotientMapLeft/Right: surjective quotient maps\n" ++
 210  "✓ REFINEMENT THEOREM: composite quotient refines both components\n" ++
 211  "✓ composite_comm: composition is commutative\n" ++
 212  "✓ Information monotonicity theorems\n" ++
 213  "\n" ++
 214  "COMPOSITION (RG6) COMPLETE"
 215
 216#eval composition_status
 217
 218end RecogGeom
 219end IndisputableMonolith
 220