nontrivial_recognition_forces_interface

formal source

 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 :