IndisputableMonolith.RecogGeom.Comparative

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Quotient
   3
   4/-!
   5# Recognition Geometry: Comparative Recognizers (RG7)
   6
   7Standard geometry assumes a pre-existing metric: you already know what "distance"
   8means. Recognition Geometry flips this: we start with recognizers that can only
   9detect qualitative relationships ("is A more than B?"), and show how metric-like
  10structure emerges.
  11
  12## The Core Insight
  13
  14A **comparative recognizer** doesn't label individual configurations; it detects
  15relationships between pairs of configurations. The simplest case:
  16- Given (c₁, c₂), output "≤" or ">"
  17
  18This is how a thermometer works: it doesn't know the absolute temperature,
  19but it can tell you which of two things is hotter.
  20
  21## Main Results
  22
  23- `ComparativeRecognizer`: Maps pairs of configurations to comparison events
  24- `RecognitionPreorder`: When comparative recognition induces a preorder
  25- `RecognitionPartialOrder`: When it induces a partial order (antisymmetric)
  26- `OrderFromComparative`: Extracting order structure from recognizers
  27- `MetricApproximation`: How metrics emerge from many comparative recognizers
  28
  29## Physical Interpretation
  30
  31In physics, most measurements are fundamentally comparative:
  32- Interference patterns compare phases
  33- Balance scales compare masses
  34- Clocks compare durations
  35
  36Recognition Geometry shows that this comparative structure is primary,
  37and absolute metrics are derived.
  38
  39-/
  40
  41namespace IndisputableMonolith
  42namespace RecogGeom
  43
  44variable {C : Type*}
  45
  46/-! ## Comparative Recognizer -/
  47
  48/-- A comparative recognizer detects relationships between pairs of configurations.
  49    It maps (c₁, c₂) to a "comparison event" that encodes their relationship. -/
  50structure ComparativeRecognizer (C E : Type*) where
  51  /-- The comparison function -/
  52  compare : C × C → E
  53  /-- Reflexivity: comparing c with itself gives a distinguished "equal" result -/
  54  eq_event : E
  55  /-- Self-comparison yields the equal event -/
  56  compare_self : ∀ c, compare (c, c) = eq_event
  57
  58/-! ## Induced Relations -/
  59
  60variable {E : Type*} [DecidableEq E]
  61
  62/-- The "not greater than" relation induced by a comparative recognizer.
  63    c₁ ≤ c₂ iff comparing them doesn't produce a "greater than" result. -/
  64def notGreaterThan (R : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
  65  R.compare (c₁, c₂) ∉ gt_events
  66
  67/-- The "equivalent" relation: neither is greater than the other -/
  68def comparativeEquiv (R : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
  69  notGreaterThan R gt_events c₁ c₂ ∧ notGreaterThan R gt_events c₂ c₁
  70
  71/-! ## Recognition Preorder -/
  72
  73/-- A comparative recognizer induces a preorder when:
  74    1. Self-comparison is "not greater than" (reflexivity)
  75    2. The relation is transitive -/
  76structure InducesPreorder (R : ComparativeRecognizer C E) (gt_events : Set E) : Prop where
  77  /-- The equal event is not a "greater than" event -/
  78  eq_not_gt : R.eq_event ∉ gt_events
  79  /-- Transitivity: c₁ ≤ c₂ and c₂ ≤ c₃ implies c₁ ≤ c₃ -/
  80  trans : ∀ c₁ c₂ c₃, notGreaterThan R gt_events c₁ c₂ →
  81                       notGreaterThan R gt_events c₂ c₃ →
  82                       notGreaterThan R gt_events c₁ c₃
  83
  84/-- When a comparative recognizer induces a preorder, we get reflexivity for free -/
  85theorem preorder_refl (R : ComparativeRecognizer C E) (gt_events : Set E)
  86    (h : InducesPreorder R gt_events) (c : C) :
  87    notGreaterThan R gt_events c c := by
  88  unfold notGreaterThan
  89  rw [R.compare_self]
  90  exact h.eq_not_gt
  91
  92/-- The induced preorder relation -/
  93def inducedPreorder (R : ComparativeRecognizer C E) (gt_events : Set E)
  94    (h : InducesPreorder R gt_events) : Preorder C where
  95  le := notGreaterThan R gt_events
  96  le_refl := preorder_refl R gt_events h
  97  le_trans := fun _ _ _ => h.trans _ _ _
  98
  99/-! ## Recognition Partial Order -/
 100
 101/-- A comparative recognizer induces a partial order when it's also antisymmetric:
 102    c₁ ≤ c₂ and c₂ ≤ c₁ implies c₁ = c₂ -/
 103structure InducesPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
 104    extends InducesPreorder R gt_events : Prop where
 105  /-- Antisymmetry -/
 106  antisymm : ∀ c₁ c₂, notGreaterThan R gt_events c₁ c₂ →
 107                       notGreaterThan R gt_events c₂ c₁ → c₁ = c₂
 108
 109/-- The induced partial order relation -/
 110def inducedPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
 111    (h : InducesPartialOrder R gt_events) : PartialOrder C where
 112  le := notGreaterThan R gt_events
 113  le_refl := preorder_refl R gt_events h.toInducesPreorder
 114  le_trans := fun _ _ _ => h.trans _ _ _
 115  le_antisymm := fun _ _ => h.antisymm _ _
 116
 117/-! ## Comparative Equivalence -/
 118
 119/-- Comparative equivalence is an equivalence relation -/
 120theorem comparativeEquiv_refl (R : ComparativeRecognizer C E) (gt_events : Set E)
 121    (h : InducesPreorder R gt_events) (c : C) :
 122    comparativeEquiv R gt_events c c :=
 123  ⟨preorder_refl R gt_events h c, preorder_refl R gt_events h c⟩
 124
 125theorem comparativeEquiv_symm (R : ComparativeRecognizer C E) (gt_events : Set E)
 126    {c₁ c₂ : C} (h : comparativeEquiv R gt_events c₁ c₂) :
 127    comparativeEquiv R gt_events c₂ c₁ :=
 128  ⟨h.2, h.1⟩
 129
 130theorem comparativeEquiv_trans (R : ComparativeRecognizer C E) (gt_events : Set E)
 131    (hp : InducesPreorder R gt_events)
 132    {c₁ c₂ c₃ : C} (h₁ : comparativeEquiv R gt_events c₁ c₂)
 133    (h₂ : comparativeEquiv R gt_events c₂ c₃) :
 134    comparativeEquiv R gt_events c₁ c₃ :=
 135  ⟨hp.trans c₁ c₂ c₃ h₁.1 h₂.1, hp.trans c₃ c₂ c₁ h₂.2 h₁.2⟩
 136
 137/-! ## Order-Respecting Recognizers -/
 138
 139/-- A standard recognizer R is compatible with a comparative recognizer R_cmp if
 140    indistinguishable configurations are also comparatively equivalent -/
 141def IsOrderCompatible (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 142    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events) : Prop :=
 143  ∀ c₁ c₂, Indistinguishable R c₁ c₂ → comparativeEquiv R_cmp gt_events c₁ c₂
 144
 145/-- If R is order-compatible, the order descends to the quotient -/
 146theorem order_descends_to_quotient (R : Recognizer C E) (R_cmp : ComparativeRecognizer C E')
 147    (gt_events : Set E') (hp : InducesPreorder R_cmp gt_events)
 148    (hcompat : IsOrderCompatible R R_cmp gt_events hp) :
 149    ∀ c₁ c₂ c₁' c₂', Indistinguishable R c₁ c₁' → Indistinguishable R c₂ c₂' →
 150      notGreaterThan R_cmp gt_events c₁ c₂ → notGreaterThan R_cmp gt_events c₁' c₂' := by
 151  intro c₁ c₂ c₁' c₂' h₁ h₂ hle
 152  have heq₁ := hcompat c₁ c₁' h₁
 153  have heq₂ := hcompat c₂ c₂' h₂
 154  -- c₁' ≤ c₁ ≤ c₂ ≤ c₂'
 155  exact hp.trans c₁' c₂ c₂' (hp.trans c₁' c₁ c₂ heq₁.2 hle) heq₂.1
 156
 157/-! ## Separation by Comparisons -/
 158
 159/-- Two configurations are separated by a comparative recognizer if they are
 160    not comparatively equivalent -/
 161def SeparatedBy (R_cmp : ComparativeRecognizer C E) (gt_events : Set E) (c₁ c₂ : C) : Prop :=
 162  ¬comparativeEquiv R_cmp gt_events c₁ c₂
 163
 164/-- A family of comparative recognizers separates points if any two distinct
 165    configurations are separated by at least one recognizer -/
 166def SeparatesPoints {ι : Type*} (R_family : ι → ComparativeRecognizer C E)
 167    (gt_events : ι → Set E) : Prop :=
 168  ∀ c₁ c₂, c₁ ≠ c₂ → ∃ i, SeparatedBy (R_family i) (gt_events i) c₁ c₂
 169
 170/-! ## Metric-Like Structure -/
 171
 172/-- A comparative recognizer defines a "distance-like" function when it can
 173    distinguish "closer" from "farther" configurations. -/
 174structure MetricCompatible (R_cmp : ComparativeRecognizer C E) (gt_events : Set E)
 175    (d : C → C → ℝ) : Prop where
 176  /-- d(c,c) = 0 -/
 177  dist_self : ∀ c, d c c = 0
 178  /-- d(c₁,c₂) ≥ 0 -/
 179  dist_nonneg : ∀ c₁ c₂, 0 ≤ d c₁ c₂
 180  /-- d(c₁,c₂) = d(c₂,c₁) -/
 181  dist_symm : ∀ c₁ c₂, d c₁ c₂ = d c₂ c₁
 182  /-- If the recognizer *separates* `c₁,c₂`, then their distance is strictly positive. -/
 183  dist_pos_of_separated : ∀ {c₁ c₂ : C}, SeparatedBy R_cmp gt_events c₁ c₂ → 0 < d c₁ c₂
 184  /-- If c₁ ≤ c₂ (by comparison), then d(c₁, c₃) ≤ d(c₂, c₃) for all c₃ -/
 185  order_respects_dist : ∀ c₁ c₂ c₃, notGreaterThan R_cmp gt_events c₁ c₂ →
 186    d c₁ c₃ ≤ d c₂ c₃
 187
 188/-- **Key Theorem**: Many comparative recognizers can approximate a metric.
 189
 190    The idea: if we have enough comparative recognizers that collectively
 191    separate all points and respect a common distance function, then
 192    that distance function is "visible" through the comparisons. -/
 193theorem metric_from_comparisons {ι : Type*} [Nonempty ι]
 194    (R_family : ι → ComparativeRecognizer C E)
 195    (gt_events : ι → Set E)
 196    (d : C → C → ℝ)
 197    (hsep : SeparatesPoints R_family gt_events)
 198    (hcompat : ∀ i, MetricCompatible (R_family i) (gt_events i) d) :
 199    -- If c₁ ≠ c₂, then d(c₁, c₂) > 0
 200    ∀ c₁ c₂, c₁ ≠ c₂ → 0 < d c₁ c₂ := by
 201  intro c₁ c₂ hne
 202  obtain ⟨i, hsep_i⟩ := hsep c₁ c₂ hne
 203  exact (hcompat i).dist_pos_of_separated hsep_i
 204
 205/-! ## The Recognition Distance -/
 206
 207/-- A recognition distance is a pseudometric derived from a family of
 208    comparative recognizers. -/
 209structure RecognitionDistance (C : Type*) where
 210  /-- The distance function -/
 211  dist : C → C → ℝ
 212  /-- Non-negativity -/
 213  dist_nonneg : ∀ c₁ c₂, 0 ≤ dist c₁ c₂
 214  /-- Self-distance is zero -/
 215  dist_self : ∀ c, dist c c = 0
 216  /-- Symmetry -/
 217  dist_symm : ∀ c₁ c₂, dist c₁ c₂ = dist c₂ c₁
 218  /-- Triangle inequality -/
 219  dist_triangle : ∀ c₁ c₂ c₃, dist c₁ c₃ ≤ dist c₁ c₂ + dist c₂ c₃
 220
 221/-- A recognition distance is a metric (not just pseudometric) when
 222    d(c₁, c₂) = 0 implies c₁ = c₂ -/
 223def RecognitionDistance.IsMetric (d : RecognitionDistance C) : Prop :=
 224  ∀ c₁ c₂, d.dist c₁ c₂ = 0 → c₁ = c₂
 225
 226/-!
 227**Physical Interpretation (documentation)**: In Recognition Science, the J-cost function
 228is intended to provide a natural recognition distance. The cost of transitioning between
 229states defines their “separation” in recognition space.
 230
 231TODO: formalize the RS bridge showing how a J-cost induces a `RecognitionDistance`.
 232-/
 233
 234/-! ## Module Status -/
 235
 236def comparative_status : String :=
 237  "✓ ComparativeRecognizer defined (RG7)\n" ++
 238  "✓ notGreaterThan, comparativeEquiv: induced relations\n" ++
 239  "✓ InducesPreorder: when comparisons give a preorder\n" ++
 240  "✓ InducesPartialOrder: when comparisons give partial order\n" ++
 241  "✓ Comparative equivalence is an equivalence relation\n" ++
 242  "✓ IsOrderCompatible: compatibility with standard recognizers\n" ++
 243  "✓ order_descends_to_quotient: order structure on quotient\n" ++
 244  "✓ SeparatesPoints: families that distinguish all configurations\n" ++
 245  "✓ MetricCompatible: when comparisons respect a metric\n" ++
 246  "✓ RecognitionDistance: pseudometric from recognition\n" ++
 247  "\n" ++
 248  "COMPARATIVE RECOGNIZERS (RG7) COMPLETE"
 249
 250#eval comparative_status
 251
 252end RecogGeom
 253end IndisputableMonolith
 254