An intrinsic interval-deletion characterization of digraph support families

Let $E$ be a finite set. A directed graph on $E$, with loops permitted, supports the subsets of $E$ in which every vertex has an in-neighbour inside the subset. The supported subsets form a union-closed family containing the empty set, and Steel (Acta Biotheoretica, 2023) asked for a set-theoretic characterization of the families that arise in this way. We give a recursive characterization that refers only to the given family $\mathcal F$. Starting from the full power set, one repeatedly selects an inclusion-maximal set $S\notin\mathcal F$, chooses a root $r\in S$ that lies in no member of $\mathcal F$ contained in $S$ and has not been used before, and deletes the interval $\{X: r\in X\subseteq S\}$. The family $\mathcal F$ is the support family of a digraph on $E$ if and only if some legal sequence of deletions ends exactly at $\mathcal F$. The residual set may be chosen by any fixed rule; only the root requires branching. Every sequence has at most $|E|$ steps, and a successful sequence reconstructs a realizing digraph on the original ground set by the predecessor rows $P(r_i)=E\setminus S_i$. The proof passes through complementation to single-head definite Horn theories, where the key step is a normalization lemma replacing one rule of a hypothetical single-head completion while preserving its models and all previously accepted rules. We derive the exact root set and length of every successful sequence, a finite recognizer whose rejections are proofs of non-realizability, membership in $\mathsf{NP}$ for explicitly listed families, closure of the class under coordinate projection (elimination of hidden vertices), induced deletion and disjoint products, a Hall-type necessary condition, and a three-element family showing that the class is not closed under intersection on a shared ground set, so that no collection of closure axioms can characterize it. For catalytic reaction systems we obtain that a family is the fixed family of an elementary system if and only if it passes the interval-deletion test, and that same-ground RAF families are exactly intersections of an antimatroid with a family passing that test. The characterization, its consequences and an executable trace checker are verified in Lean 4.