Dominator Cut

Abstract

A dominator is a vertex whose deletion cuts every rooted path to its target.

Theorem 1.1 (Deleting a proper dominator makes the target unreachable).

$$\begin{array}{c}\forall edge:V\to V\to \mathrm{Prop},\\ root,u,v:V,\\ (\mathrm{Dominates}\left(root,edge,u,v\right)\wedge u\ne v)\Rightarrow \\ \neg \mathrm{Nonempty}\left(\mathrm{DirectedPath}\left(\mathrm{deleteVertex}\left(edge,u\right),root,v\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DependencyTopology/DominatorCut.unreachable_after_delete_of_dominates (✓ std3). ∎

Source. Repository-derived.

Commentary.

Dominates means that every directed path from the root to the target contains the designated vertex.

Deleting that vertex retains only edges whose endpoints are both different from it. Any path in the deleted graph maps back to an original path that avoids the deleted vertex.

When the dominator is distinct from the target, such an avoiding path contradicts dominance. Therefore the deleted graph has no rooted directed path to the target.

References

• Truth anchor: D5/S3/ConceptDynamics/DependencyTopology/DominatorCut.unreachable_after_delete_of_dominates