module module

`IndisputableMonolith.Foundation.ObserverForcing`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (20)

structure RecognitionEvent L44
def cost L51
theorem cost_nonneg L54
def identity L58
theorem identity_cost L63
structure CoherentRecognition L74
def IsPersistent L90
theorem identity_persistent L93
theorem persistent_state_unique L97
theorem persistent_event_state_eq_identity L105
theorem cooper_pair_cost_zero L117
theorem cooper_pairing_yields_persistent L124
structure Observer L141
theorem reference_zero_cost L148
theorem reference_unit_state L153
theorem has_distinguishable_events L158
theorem nontrivial_recognition_forces_observer L175
theorem cooper_paired_reference_yields_observer L194
theorem observer_forcing_certificate L227
def observer_forcing_status L251