module module

`IndisputableMonolith.Verification.Necessity.ConservationNecessity`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Recognition module_import
IndisputableMonolith.Verification.Exclusivity.Framework module_import

declarations in this module (23)

theorem recognition_requires_distinguishability_proven L28
structure DiscreteEventSystem L51
structure EventEvolution L56
structure FlowFS L61
def NonTrivialFlow L65
def Distinguishable L70
structure RecognitionEvent L77
def HasRecognitionEvents L84
theorem mp_implies_recognition_meaningful L97
theorem nontrivial_system_has_recognition_events L106
lemma distinction_implies_flow_structure L120
def FlowOnEdge L134
lemma flow_on_edge_nontrivial L139
theorem mp_forces_nontrivial_flow_exists L150
def RecognitionFlow L168
lemma recognition_flow_nontrivial L173
theorem recognition_implies_nontrivial_flow_exists L184
def IsRecognitionFlow L202
lemma recognition_flow_distinguishable L207
theorem recognition_flow_implies_distinguishable L216
theorem mp_forces_distinguishable_flow_exists L230
theorem conservation_necessity_proven L245
def conservation_necessity_status L266