reference_zero_cost

formal source

 145namespace Observer
 146
 147/-- An observer's reference has zero cost. -/
 148theorem reference_zero_cost (obs : Observer) :
 149    obs.recognition.reference.cost = 0 :=
 150  obs.persistent
 151
 152/-- An observer's reference state is exactly `x = 1`. -/
 153theorem reference_unit_state (obs : Observer) :
 154    obs.recognition.reference.state = 1 :=
 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