pith. machine review for the scientific record. sign in
theorem proved term proof

nontrivial_recognition_forces_observer

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (26)

Lean names referenced from this declaration's body.