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

observer_forcing_certificate

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)

 227theorem observer_forcing_certificate :
 228    -- (1) Cost is non-negative
 229    (∀ e : RecognitionEvent, 0 ≤ e.cost) ∧
 230    -- (2) Identity event has zero cost
 231    RecognitionEvent.identity.cost = 0 ∧
 232    -- (3) Identity event is persistent
 233    IsPersistent RecognitionEvent.identity ∧
 234    -- (4) Persistent state is unique (= 1)
 235    (∀ ref : RecognitionEvent, IsPersistent ref → ref.state = 1) ∧
 236    -- (5) Cooper pairing yields persistence for any positive x
 237    (∀ x : ℝ, 0 < x → ∃ e : RecognitionEvent, IsPersistent e) ∧
 238    -- (6) Non-trivial recognition forces an observer
 239    (∀ (events : ℕ → RecognitionEvent),
 240       (∃ n m : ℕ, (events n).state ≠ (events m).state) →
 241       ∃ obs : Observer, obs.recognition.events = events) :=

proof body

Term-mode proof.

 242  ⟨RecognitionEvent.cost_nonneg,
 243   RecognitionEvent.identity_cost,
 244   identity_persistent,
 245   persistent_state_unique,
 246   cooper_pairing_yields_persistent,
 247   nontrivial_recognition_forces_observer⟩
 248
 249/-! ## Module Status -/
 250

depends on (27)

Lean names referenced from this declaration's body.