has_distinguishable_events

formal source

 155  persistent_state_unique obs.recognition.reference obs.persistent
 156
 157/-- An observer always carries at least two distinguishable events. -/
 158theorem has_distinguishable_events (obs : Observer) :
 159    ∃ n m : ℕ, (obs.recognition.events n).state ≠ (obs.recognition.events m).state :=
 160  obs.recognition.nontrivial
 161
 162end Observer
 163
 164/-! ## §6. The Master Forcing Theorem -/
 165
 166/-- **Observer-Forcing Theorem.** Every non-trivial recognition stream
 167    forces the existence of an observer.
 168
 169    Given any sequence of recognition events that contains at least
 170    two distinguishable states, an observer can be constructed whose
 171    recognition stream is exactly that sequence and whose reference is
 172    the canonical identity-tick event. The observer is not an
 173    external posit. It is forced by the structural requirements of
 174    coherent multi-event recognition. -/
 175theorem nontrivial_recognition_forces_observer
 176    (events : ℕ → RecognitionEvent)
 177    (h_nontrivial : ∃ n m : ℕ, (events n).state ≠ (events m).state) :
 178    ∃ obs : Observer, obs.recognition.events = events := by
 179  refine ⟨{
 180    recognition := {
 181      events := events,
 182      reference := RecognitionEvent.identity,
 183      nontrivial := h_nontrivial
 184    },
 185    persistent := identity_persistent
 186  }, rfl⟩
 187
 188/-! ## §7. Strengthening: Cooper-Paired Reference -/