158theorem has_distinguishable_events (obs : Observer) : 159 ∃ n m : ℕ, (obs.recognition.events n).state ≠ (obs.recognition.events m).state :=
proof body
Term-mode proof.
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. -/
depends on (25)
Lean names referenced from this declaration's body.