IndisputableMonolith.RecogGeom.Examples

   1import Mathlib
   2import IndisputableMonolith.RecogGeom.Core
   3import IndisputableMonolith.RecogGeom.Recognizer
   4import IndisputableMonolith.RecogGeom.Indistinguishable
   5import IndisputableMonolith.RecogGeom.Quotient
   6
   7/-!
   8# Recognition Geometry: Concrete Examples
   9
  10A geometry isn't complete without examples. This module provides concrete
  11recognition geometries that illustrate the framework.
  12
  13## Examples Developed
  14
  151. **Discrete Recognition on Fin n** - Every config distinguishable
  162. **Sign Recognizer on ℤ** - Three equivalence classes (neg, zero, pos)
  173. **Magnitude Recognizer on ℤ** - |n| determines the class
  18
  19## Key Insights from Examples
  20
  21- Discrete recognizer: quotient ≅ original space
  22- Sign recognizer: ℤ/~ has exactly 3 classes
  23- Magnitude recognizer: infinitely many classes (0, 1, 2, ...)
  24- Composition refines: sign ⊗ magnitude distinguishes more
  25
  26-/
  27
  28namespace IndisputableMonolith
  29namespace RecogGeom
  30namespace Examples
  31
  32/-! ## Example 1: Discrete Recognition on Fin n -/
  33
  34/-- Configuration space: Fin n (n ≥ 2 distinct configurations) -/
  35instance finConfigSpace (n : ℕ) [h : NeZero n] : ConfigSpace (Fin n) where
  36  nonempty := ⟨0⟩
  37
  38/-- The discrete recognizer: identity map (distinguishes everything) -/
  39def discreteRecognizer (n : ℕ) [h : NeZero n] (hn : 2 ≤ n) :
  40    Recognizer (Fin n) (Fin n) where
  41  R := id
  42  nontrivial := by
  43    use ⟨0, by omega⟩, ⟨1, by omega⟩
  44    simp [Fin.ext_iff]
  45
  46/-- **Theorem**: Discrete recognizer - indistinguishable iff equal -/
  47theorem discrete_indist_iff_eq (n : ℕ) [h : NeZero n] (hn : 2 ≤ n)
  48    (c₁ c₂ : Fin n) :
  49    Indistinguishable (discreteRecognizer n hn) c₁ c₂ ↔ c₁ = c₂ := by
  50  simp [Indistinguishable, discreteRecognizer]
  51
  52/-- **Corollary**: Each config is in its own resolution cell -/
  53theorem discrete_singleton_cells (n : ℕ) [h : NeZero n] (hn : 2 ≤ n) (c : Fin n) :
  54    ResolutionCell (discreteRecognizer n hn) c = {c} := by
  55  ext x
  56  simp [ResolutionCell, discrete_indist_iff_eq]
  57
  58/-! ## Example 2: Sign Recognizer on ℤ -/
  59
  60/-- Integer configuration space -/
  61instance : ConfigSpace ℤ where
  62  nonempty := ⟨0⟩
  63
  64/-- Three-valued sign type -/
  65inductive Sign : Type
  66  | neg : Sign
  67  | zero : Sign
  68  | pos : Sign
  69  deriving DecidableEq, Repr
  70
  71/-- Sign is nonempty -/
  72instance : Nonempty Sign := ⟨Sign.zero⟩
  73
  74/-- The sign function -/
  75def signOf : ℤ → Sign
  76  | n => if n < 0 then Sign.neg else if n = 0 then Sign.zero else Sign.pos
  77
  78/-- The sign recognizer on ℤ -/
  79def signRecognizer : Recognizer ℤ Sign where
  80  R := signOf
  81  nontrivial := by
  82    use -1, 1
  83    simp [signOf]
  84
  85/-- **Theorem**: Two integers are indistinguishable iff same sign -/
  86theorem sign_indistinguishable (n m : ℤ) :
  87    Indistinguishable signRecognizer n m ↔ signOf n = signOf m := by
  88  rfl
  89
  90/-- **Theorem**: -5 ~ -3 (both negative) -/
  91theorem neg_indist : Indistinguishable signRecognizer (-5) (-3) := by
  92  simp [Indistinguishable, signRecognizer, signOf]
  93
  94/-- **Theorem**: -1 ≁ 1 (different signs) -/
  95theorem neg_pos_dist : ¬Indistinguishable signRecognizer (-1) 1 := by
  96  simp [Indistinguishable, signRecognizer, signOf]
  97
  98/-- **Theorem**: 0 ≁ 1 (different signs) -/
  99theorem zero_pos_dist : ¬Indistinguishable signRecognizer 0 1 := by
 100  simp [Indistinguishable, signRecognizer, signOf]
 101
 102/-! ## Example 3: Magnitude Recognizer on ℤ -/
 103
 104/-- The magnitude recognizer: n ↦ |n| -/
 105def magnitudeRecognizer : Recognizer ℤ ℕ where
 106  R := fun n => n.natAbs
 107  nontrivial := by
 108    use 0, 1
 109    simp
 110
 111/-- **Theorem**: n ~ m iff |n| = |m| -/
 112theorem magnitude_indistinguishable (n m : ℤ) :
 113    Indistinguishable magnitudeRecognizer n m ↔ n.natAbs = m.natAbs := by
 114  rfl
 115
 116/-- **Theorem**: 3 ~ -3 (same magnitude) -/
 117theorem plus_minus_indist : Indistinguishable magnitudeRecognizer 3 (-3) := by
 118  simp [Indistinguishable, magnitudeRecognizer]
 119
 120/-- **Theorem**: 2 ≁ 3 (different magnitudes) -/
 121theorem diff_magnitude_dist : ¬Indistinguishable magnitudeRecognizer 2 3 := by
 122  simp [Indistinguishable, magnitudeRecognizer]
 123
 124/-! ## Example 4: Composition Refines Both -/
 125
 126/-- **Key Observation**: Combining sign and magnitude gives a finer recognizer.
 127
 128    - Sign alone: 3 ~ -3 (both positive/negative)... wait, that's wrong
 129    - Actually sign: 3 ≁ -3 (positive vs negative)
 130    - Magnitude alone: 3 ~ -3 (both have magnitude 3)
 131
 132    So sign distinguishes 3 from -3, but magnitude doesn't.
 133    Conversely, magnitude distinguishes 3 from 5, both positive.
 134
 135    The composition (sign, magnitude) distinguishes both. -/
 136theorem sign_distinguishes_3_neg3 : ¬Indistinguishable signRecognizer 3 (-3) := by
 137  simp [Indistinguishable, signRecognizer, signOf]
 138
 139theorem magnitude_indist_3_neg3 : Indistinguishable magnitudeRecognizer 3 (-3) := by
 140  simp [Indistinguishable, magnitudeRecognizer]
 141
 142theorem sign_indist_3_5 : Indistinguishable signRecognizer 3 5 := by
 143  simp [Indistinguishable, signRecognizer, signOf]
 144
 145theorem magnitude_distinguishes_3_5 : ¬Indistinguishable magnitudeRecognizer 3 5 := by
 146  simp [Indistinguishable, magnitudeRecognizer]
 147
 148/-- **Composition Principle**: Neither sign nor magnitude alone distinguishes
 149    all pairs, but together they do (for nonzero integers). -/
 150theorem composition_refines :
 151    (∀ n m : ℤ, n ≠ 0 → m ≠ 0 →
 152      (Indistinguishable signRecognizer n m ∧ Indistinguishable magnitudeRecognizer n m) →
 153      n = m ∨ n = -m) := by
 154  intro n m hn hm ⟨hsign, hmag⟩
 155  simp only [Indistinguishable, signRecognizer, magnitudeRecognizer] at hsign hmag
 156  -- Same sign and same magnitude implies n = m or n = -m
 157  have h1 : n.natAbs = m.natAbs := hmag
 158  -- If signs match and magnitudes match, must be equal or negatives
 159  rcases Int.natAbs_eq_natAbs_iff.mp h1 with h | h
 160  · left; exact h
 161  · right; exact h
 162
 163/-! ## Physical Interpretation -/
 164
 165/-! ### Physical Interpretation
 166
 167These examples show how recognizers model measurement in physics:
 168- **Discrete** = perfect measurement (eigenvalue detection)
 169- **Sign/magnitude** = coarse measurements (binary outcomes)
 170- **Composition** = combined measurements with finer resolution
 171
 172In quantum mechanics, observables ARE recognizers mapping states to eigenvalues. -/
 173
 174/-! ## Module Status -/
 175
 176def examples_status : String :=
 177  "✓ Discrete Recognition on Fin n\n" ++
 178  "  • discrete_indist_iff_eq: indistinguishable ↔ equal\n" ++
 179  "  • discrete_singleton_cells: each config is its own cell\n" ++
 180  "\n" ++
 181  "✓ Sign Recognizer on ℤ\n" ++
 182  "  • sign_indistinguishable: same sign ↔ indistinguishable\n" ++
 183  "  • neg_indist, neg_pos_dist: concrete examples\n" ++
 184  "\n" ++
 185  "✓ Magnitude Recognizer on ℤ\n" ++
 186  "  • magnitude_indistinguishable: same |n| ↔ indistinguishable\n" ++
 187  "  • plus_minus_indist: 3 ~ -3\n" ++
 188  "\n" ++
 189  "✓ Composition Analysis\n" ++
 190  "  • sign_distinguishes_3_neg3 vs magnitude_indist_3_neg3\n" ++
 191  "  • sign_indist_3_5 vs magnitude_distinguishes_3_5\n" ++
 192  "  • composition_refines: combining gives finer resolution\n" ++
 193  "\n" ++
 194  "EXAMPLES COMPLETE"
 195
 196#eval examples_status
 197
 198end Examples
 199end RecogGeom
 200end IndisputableMonolith
 201