theorem proved term proof

`reference_unit_state`

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

formal statement (Lean)

 153theorem reference_unit_state (obs : Observer) :
 154    obs.recognition.reference.state = 1 :=

proof body

Term-mode proof.

 155  persistent_state_unique obs.recognition.reference obs.persistent
 156
 157/-- An observer always carries at least two distinguishable events. -/

depends on (4)

Lean names referenced from this declaration's body.

Observer in IndisputableMonolith.Foundation.Determinism decl_use
Observer in IndisputableMonolith.Foundation.ObserverForcing decl_use
persistent_state_unique in IndisputableMonolith.Foundation.ObserverForcing decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use