 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.