ObserverFromRecognitionCert

formal source

 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