IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer

   1import Mathlib
   2import IndisputableMonolith.Foundation.ObserverFromRecognition
   3import IndisputableMonolith.Foundation.ArithmeticFromLogic
   4
   5/-!
   6# Recognition Lattice from a Recognizer
   7
   8This module turns the structural claim of Recognition Geometry into a Lean
   9theorem:
  10
  11> a recognizer's kernel-equivalence classes are the first recognition lattice.
  12
  13The lattice here is pre-spatial. It is the quotient of the carrier by the
  14primitive observer's indistinguishability kernel. The cells are equivalence
  15classes of configurations that the recognizer cannot tell apart. Finite
  16resolution is inherited from the finite event codomain `Fin n`.
  17
  18## Honest scope
  19
  20The lattice produced here is the **recognition quotient lattice**, not yet a
  21metric/topological manifold. It proves:
  22
  23* existence of the lattice for any primitive interface;
  24* existence of such a lattice from any non-trivial recognition event;
  25* finite-resolution neighborhoods from event labels;
  26* uniqueness up to canonical equivalence for interfaces with the same kernel;
  27* interpretation of the universal iteration object `LogicNat` into the lattice.
  28
  29Since the lattice can be finite (e.g. a two-outcome recognizer), the
  30`LogicNat` map is an interpretation, not an embedding/injection. This is the
  31same distinction as the Boolean parity collapse in Universal Forcing: the
  32iteration object remains free, while its image in a finite carrier may
  33collapse.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Foundation
  38namespace RecognitionLatticeFromRecognizer
  39
  40open Classical
  41open ObserverFromRecognition
  42open ArithmeticFromLogic
  43
  44/-! ## Kernel quotient -/
  45
  46/-- The setoid induced by a primitive interface. Two configurations are
  47equivalent iff the interface sends them to the same event. -/
  48def interfaceSetoid {K : Type*} (I : PrimitiveInterface K) : Setoid K where
  49  r := I.kernel
  50  iseqv := kernel_is_equivalence I
  51
  52/-- The **recognition lattice** generated by an interface: the quotient by
  53the interface kernel. -/
  54def RecognitionLattice {K : Type*} (I : PrimitiveInterface K) : Type _ :=
  55  Quotient (interfaceSetoid I)
  56
  57/-- The lattice cell containing a configuration. -/
  58def cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :
  59    RecognitionLattice I :=
  60  Quotient.mk (interfaceSetoid I) x
  61
  62/-- Two configurations determine the same cell iff the recognizer cannot
  63distinguish them. -/
  64theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
  65    cellOf I x = cellOf I y ↔ I.kernel x y := by
  66  exact Quotient.eq
  67
  68/-! ## Finite-resolution labels and neighborhoods -/
  69
  70/-- The finite event label of a recognition cell. This is well-defined because
  71the quotient identifies exactly configurations with equal observed labels. -/
  72def cellLabel {K : Type*} (I : PrimitiveInterface K) :
  73    RecognitionLattice I → Fin I.n :=
  74  Quotient.lift (fun x => I.observe x) (by
  75    intro x y h
  76    exact h)
  77
  78@[simp] theorem cellLabel_cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :
  79    cellLabel I (cellOf I x) = I.observe x := rfl
  80
  81/-- A finite-resolution neighborhood: all cells with a given observed label. -/
  82def neighborhood {K : Type*} (I : PrimitiveInterface K) (label : Fin I.n) :
  83    Set (RecognitionLattice I) :=
  84  { c | cellLabel I c = label }
  85
  86/-- The cell of a configuration lies in the neighborhood of its observed label. -/
  87theorem cell_mem_own_neighborhood {K : Type*} (I : PrimitiveInterface K) (x : K) :
  88    cellOf I x ∈ neighborhood I (I.observe x) := by
  89  simp [neighborhood]
  90
  91/-- Every lattice cell has a finite-resolution label. -/
  92theorem every_cell_has_label {K : Type*} (I : PrimitiveInterface K)
  93    (c : RecognitionLattice I) :
  94    ∃ label : Fin I.n, c ∈ neighborhood I label := by
  95  refine ⟨cellLabel I c, ?_⟩
  96  simp [neighborhood]
  97
  98/-! ## Existence from non-trivial recognition -/
  99
 100/-- A non-trivial recognition event forces a recognition lattice. -/
 101theorem nontrivial_recognition_forces_lattice (K : Type*) :
 102    NontrivialRecognition K →
 103    ∃ (I : PrimitiveInterface K), Nonempty (RecognitionLattice I) := by
 104  intro h
 105  obtain ⟨I, x, _y, _hdist, _hsep⟩ := nontrivial_recognition_forces_interface K h
 106  exact ⟨I, ⟨cellOf I x⟩⟩
 107
 108/-- The minimal two-outcome lattice forced by a distinguished point. -/
 109noncomputable def pointLattice {K : Type*} (x₀ : K) : Type _ :=
 110  RecognitionLattice (pointInterface x₀)
 111
 112/-! ## Uniqueness up to canonical equivalence -/
 113
 114/-- Two primitive interfaces have the same kernel if they make the same
 115distinctions invisible. -/
 116def SameKernel {K : Type*} (I J : PrimitiveInterface K) : Prop :=
 117  ∀ x y : K, I.kernel x y ↔ J.kernel x y
 118
 119/-- If two interfaces have the same kernel, then their recognition lattices
 120are canonically equivalent. -/
 121noncomputable def latticeEquivOfSameKernel {K : Type*}
 122    (I J : PrimitiveInterface K) (h : SameKernel I J) :
 123    RecognitionLattice I ≃ RecognitionLattice J where
 124  toFun := Quotient.map (fun x => x) (by
 125    intro x y hxy
 126    exact (h x y).mp hxy)
 127  invFun := Quotient.map (fun x => x) (by
 128    intro x y hxy
 129    exact (h x y).mpr hxy)
 130  left_inv := by
 131    intro c
 132    refine Quotient.inductionOn c ?_
 133    intro x
 134    rfl
 135  right_inv := by
 136    intro c
 137    refine Quotient.inductionOn c ?_
 138    intro x
 139    rfl
 140
 141/-- The canonical equivalence sends each cell to the cell of the same
 142configuration. -/
 143theorem latticeEquivOfSameKernel_cell {K : Type*}
 144    (I J : PrimitiveInterface K) (h : SameKernel I J) (x : K) :
 145    latticeEquivOfSameKernel I J h (cellOf I x) = cellOf J x := rfl
 146
 147/-! ## LogicNat interpretation into the lattice -/
 148
 149/-- The carrier representative of an iterated recognition step. -/
 150def iteratedCarrier {K : Type*} (base : K) (step : K → K) : LogicNat → K
 151  | LogicNat.identity => base
 152  | LogicNat.step n => step (iteratedCarrier base step n)
 153
 154/-- The canonical interpretation of `LogicNat` into a recognition lattice. -/
 155def logicNatToLattice {K : Type*} (I : PrimitiveInterface K)
 156    (base : K) (step : K → K) : LogicNat → RecognitionLattice I :=
 157  fun n => cellOf I (iteratedCarrier base step n)
 158
 159@[simp] theorem logicNatToLattice_zero {K : Type*}
 160    (I : PrimitiveInterface K) (base : K) (step : K → K) :
 161    logicNatToLattice I base step LogicNat.identity = cellOf I base := rfl
 162
 163@[simp] theorem logicNatToLattice_step {K : Type*}
 164    (I : PrimitiveInterface K) (base : K) (step : K → K) (n : LogicNat) :
 165    logicNatToLattice I base step (LogicNat.step n) =
 166      cellOf I (step (iteratedCarrier base step n)) := rfl
 167
 168/-- Every primitive interface admits a `LogicNat` interpretation into its
 169recognition lattice as soon as a base point and a step function are chosen. -/
 170theorem logicNat_interprets_into_lattice {K : Type*}
 171    (I : PrimitiveInterface K) (base : K) (step : K → K) :
 172    ∃ interp : LogicNat → RecognitionLattice I,
 173      interp LogicNat.identity = cellOf I base ∧
 174      ∀ n, interp (LogicNat.step n) =
 175        cellOf I (step (iteratedCarrier base step n)) := by
 176  exact ⟨logicNatToLattice I base step, rfl, fun _ => rfl⟩
 177
 178/-! ## Certificate -/
 179
 180structure RecognitionLatticeCert (K : Type*) where
 181  from_nontrivial :
 182    NontrivialRecognition K → ∃ I : PrimitiveInterface K, Nonempty (RecognitionLattice I)
 183  kernel_equiv :
 184    ∀ I : PrimitiveInterface K, Equivalence I.kernel
 185  every_cell_labeled :
 186    ∀ (I : PrimitiveInterface K) (c : RecognitionLattice I),
 187      ∃ label : Fin I.n, c ∈ neighborhood I label
 188  same_kernel_unique :
 189    ∀ (I J : PrimitiveInterface K), SameKernel I J →
 190      RecognitionLattice I ≃ RecognitionLattice J
 191  logicNat_interpretation :
 192    ∀ (I : PrimitiveInterface K) (base : K) (step : K → K),
 193      ∃ interp : LogicNat → RecognitionLattice I,
 194        interp LogicNat.identity = cellOf I base ∧
 195        ∀ n, interp (LogicNat.step n) =
 196          cellOf I (step (iteratedCarrier base step n))
 197
 198noncomputable def recognitionLatticeCert (K : Type*) : RecognitionLatticeCert K where
 199  from_nontrivial := nontrivial_recognition_forces_lattice K
 200  kernel_equiv := kernel_is_equivalence
 201  every_cell_labeled := every_cell_has_label
 202  same_kernel_unique := latticeEquivOfSameKernel
 203  logicNat_interpretation := logicNat_interprets_into_lattice
 204
 205theorem recognitionLatticeCert_inhabited (K : Type*) :
 206    Nonempty (RecognitionLatticeCert K) :=
 207  ⟨recognitionLatticeCert K⟩
 208
 209/-!
 210## Summary
 211
 212The lattice is no longer a prose object:
 213
 214```
 215non-trivial recognition
 216  → primitive interface
 217  → kernel equivalence relation
 218  → quotient cells
 219  → finite-resolution neighborhoods
 220  → recognition lattice
 221  → LogicNat interpretation
 222```
 223
 224This module is the Lean bridge from primitive observer/interface to the
 225recognition lattice used in Recognition Geometry.
 226-/
 227
 228end RecognitionLatticeFromRecognizer
 229end Foundation
 230end IndisputableMonolith
 231