An intrinsic interval-deletion characterization of digraph support families

For a finite directed graph with loops allowed, its supported subsets are those in which every vertex has an in-neighbour within the subset. We characterize exactly which set families arise this way on their original ground set. Starting from the power set, a legal step chooses an inclusion-maximal remaining nonmember, selects a previously unused root absent from every target-family member below it, and deletes the rooted interval. A family is a digraph support family if and only if some legal deletion sequence reaches it. The maximal residual set may follow any fixed valid policy; only roots require branching. Successful traces have at most one step per vertex and reconstruct a realizing digraph. Consequences include exact root sets and trace length, a finite recognizer, conventional NP membership for explicit lists, projection, deletion and product closure, and RAF realizability criteria using the published antimatroid characterization. The characterization and selected consequences and trace-checking interfaces are verified in Lean 4; conventional statements and computational examples are identified separately.