IndisputableMonolith.Foundation.ObserverFromRecognition

   1import Mathlib
   2import IndisputableMonolith.Foundation.PrimitiveDistinction
   3
   4/-!
   5# Observer From Recognition
   6
   7This module proves the next foundational step:
   8
   9> non-trivial recognition forces an interface, and an interface is the
  10> primitive observer.
  11
  12The word "observer" here is not yet a biological observer or a
  13physical measuring device. It is the minimal interface through
  14which a distinction becomes an event. The theorem says that once a carrier has
  15even one non-trivial distinction, there exists a finite-valued recognizer that
  16separates the distinguished pair. That finite-valued recognizer is the
  17primitive observer-like structure.
  18
  19In the later physical theory, `ObserverFormalization.lean` upgrades this
  20primitive interface into a finite-resolution recognizer over ledger
  21configurations. This module supplies the pre-physical floor.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Foundation
  26namespace ObserverFromRecognition
  27
  28open Classical
  29open PrimitiveDistinction
  30
  31/-! ## Primitive Interface -/
  32
  33/-- A primitive interface on a carrier `K`: a finite-valued recognizer.
  34
  35The codomain is `Fin n`, so the interface has finite resolution. This is the
  36pre-physical form of an observer: not a mind, but the map through which
  37configurations become distinguishable events. -/
  38structure PrimitiveInterface (K : Type*) where
  39  n : ℕ
  40  hpos : 0 < n
  41  observe : K → Fin n
  42
  43/-- The kernel of an interface: two configurations are indistinguishable
  44relative to the interface iff they produce the same observed outcome. -/
  45def PrimitiveInterface.kernel {K : Type*} (I : PrimitiveInterface K)
  46    (x y : K) : Prop :=
  47  I.observe x = I.observe y
  48
  49/-- A primitive observer is exactly a primitive interface. This is a naming
  50choice, but it is important: the observer is not external to recognition; it is
  51the interface structure recognition forces. -/
  52abbrev PrimitiveObserver (K : Type*) := PrimitiveInterface K
  53
  54/-- The observer kernel is reflexive. -/
  55theorem kernel_refl {K : Type*} (I : PrimitiveInterface K) (x : K) :
  56    I.kernel x x := rfl
  57
  58/-- The observer kernel is symmetric. -/
  59theorem kernel_symm {K : Type*} (I : PrimitiveInterface K) {x y : K}
  60    (h : I.kernel x y) : I.kernel y x := h.symm
  61
  62/-- The observer kernel is transitive. -/
  63theorem kernel_trans {K : Type*} (I : PrimitiveInterface K) {x y z : K}
  64    (hxy : I.kernel x y) (hyz : I.kernel y z) : I.kernel x z :=
  65  hxy.trans hyz
  66
  67/-- Every primitive interface partitions its carrier into observational
  68equivalence classes. -/
  69theorem kernel_is_equivalence {K : Type*} (I : PrimitiveInterface K) :
  70    Equivalence (I.kernel) :=
  71  ⟨kernel_refl I,
  72   fun {x y} h => kernel_symm I (x := x) (y := y) h,
  73   fun {x y z} h₁ h₂ => kernel_trans I (x := x) (y := y) (z := z) h₁ h₂⟩
  74
  75/-! ## Non-Trivial Recognition -/
  76
  77/-- A carrier has non-trivial recognition when at least two configurations are
  78distinguishable. At the primitive floor this is simply the existence of a
  79non-equality. -/
  80def NontrivialRecognition (K : Type*) : Prop :=
  81  ∃ x y : K, equalityDistinction K x y
  82
  83/-- An interface separates a pair if the pair lands in distinct observed
  84outcomes. -/
  85def Separates {K : Type*} (I : PrimitiveInterface K) (x y : K) : Prop :=
  86  I.observe x ≠ I.observe y
  87
  88/-- The canonical two-outcome interface that asks whether the input is the
  89chosen reference point `x₀`. This is the minimal finite recognizer induced by
  90one named distinction. -/
  91noncomputable def pointInterface {K : Type*} (x₀ : K) :
  92    PrimitiveInterface K where
  93  n := 2
  94  hpos := by norm_num
  95  observe := fun x =>
  96    if x = x₀ then (1 : Fin 2) else (0 : Fin 2)
  97
  98/-- The point interface recognizes its reference point as outcome `1`. -/
  99theorem pointInterface_at_ref {K : Type*} (x₀ : K) :
 100    (pointInterface x₀).observe x₀ = (1 : Fin 2) := by
 101  unfold pointInterface
 102  simp
 103
 104/-- Any point distinct from the reference is recognized as outcome `0`. -/
 105theorem pointInterface_away {K : Type*} {x₀ y : K} (h : y ≠ x₀) :
 106    (pointInterface x₀).observe y = (0 : Fin 2) := by
 107  unfold pointInterface
 108  simp [h]
 109
 110/-- The point interface separates any point from any distinct point. -/
 111theorem pointInterface_separates {K : Type*} {x₀ y : K} (h : x₀ ≠ y) :
 112    Separates (pointInterface x₀) x₀ y := by
 113  unfold Separates
 114  rw [pointInterface_at_ref x₀]
 115  have hy : y ≠ x₀ := fun h' => h h'.symm
 116  rw [pointInterface_away hy]
 117  norm_num
 118
 119/-! ## Main Theorem -/
 120
 121/-- **Observer from recognition.**
 122
 123If a carrier admits any non-trivial recognition, then there exists a finite
 124interface, hence a primitive observer, that separates a distinguished pair.
 125
 126This is the pre-physical observer theorem: observer-dependence is not added
 127at the quantum-measurement layer. It is forced at the first moment a
 128distinction becomes an event. -/
 129theorem nontrivial_recognition_forces_interface (K : Type*) :
 130    NontrivialRecognition K →
 131    ∃ (I : PrimitiveInterface K) (x y : K),
 132      equalityDistinction K x y ∧ Separates I x y := by
 133  intro h
 134  rcases h with ⟨x, y, hxy⟩
 135  exact ⟨pointInterface x, x, y, hxy, pointInterface_separates hxy⟩
 136
 137/-- Same theorem under the observer name: non-trivial recognition forces a
 138primitive observer. -/
 139theorem nontrivial_recognition_forces_observer (K : Type*) :
 140    NontrivialRecognition K →
 141    ∃ (O : PrimitiveObserver K) (x y : K),
 142      equalityDistinction K x y ∧ Separates O x y :=
 143  nontrivial_recognition_forces_interface K
 144
 145/-- The primitive observer theorem in compact certificate form. -/
 146structure ObserverFromRecognitionCert where
 147  forced :
 148    ∀ K : Type*, NontrivialRecognition K →
 149      ∃ (O : PrimitiveObserver K) (x y : K),
 150        equalityDistinction K x y ∧ Separates O x y
 151  kernel_equiv :
 152    ∀ {K : Type*} (O : PrimitiveObserver K), Equivalence (O.kernel)
 153
 154/-- Certificate: the primitive observer is forced by non-trivial recognition. -/
 155def observerFromRecognitionCert : ObserverFromRecognitionCert where
 156  forced := nontrivial_recognition_forces_observer
 157  kernel_equiv := kernel_is_equivalence
 158
 159theorem observerFromRecognitionCert_inhabited :
 160    Nonempty ObserverFromRecognitionCert :=
 161  ⟨observerFromRecognitionCert⟩
 162
 163/-! ## Relation to the pre-temporal order
 164
 165`PreTemporalForcingOrder.lean` records that the primitive observer, in this
 166sense, precedes time and physical light. The embodied observer of
 167`ObserverFormalization.lean` is downstream: a physical finite-resolution
 168interface living inside the ledger and spacetime structure.
 169-/
 170
 171end ObserverFromRecognition
 172end Foundation
 173end IndisputableMonolith
 174