nontrivial_recognition_forces_observer

formal source

 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 -/
 189
 190/-- An alternative observer construction: instead of using the canonical
 191    identity event as the reference, use a Cooper-paired event built
 192    from any positive state. The resulting observer is still a valid
 193    observer because the Cooper pair sits at the J-cost minimum. -/
 194theorem cooper_paired_reference_yields_observer
 195    (events : ℕ → RecognitionEvent)
 196    (h_nontrivial : ∃ n m : ℕ, (events n).state ≠ (events m).state)
 197    (x : ℝ) (hx : 0 < x) :
 198    ∃ obs : Observer, obs.recognition.events = events := by
 199  obtain ⟨ref, hpref⟩ := cooper_pairing_yields_persistent x hx
 200  refine ⟨{
 201    recognition := {
 202      events := events,
 203      reference := ref,
 204      nontrivial := h_nontrivial
 205    },