Ordered DFS execution with local timestamp and label invariants

Let $G$ be a represented finite directed multigraph, with $n$ vertices and $m$ adjacency occurrences, in an arbitrary initial heap. Let an allocated input sequence have a vertex permutation in its first $n$ entries. The generated ordered recursive DFS has a completed call, valid under every suspended caller stack, returning a fresh result object and six distinct fresh arrays. All initial sequences, objects, and collections are preserved, allocation counters and the work clock do not decrease, and other clocks are unchanged. The completed call satisfies

Its returned colors are black, its event clock and finish count are $2n$ and $n$, and its tree count is at most $n$. Its parent, discovery, finish, increasing-finish order, and tree-label arrays satisfy the local certificate: distinct valid event times with nested or disjoint intervals; parent edges and strictly containing parent intervals; the nearest-enclosing-parent condition; discovery of every edge target before its source finishes; root priority; increasing permutation of finish times; dense bounded labels inherited across parent links; and label order agreeing with discovery order at roots.

The certificate contains no parent-path or white-path equivalence and no common-root characterization of equal labels. These global properties can be established separately from the local invariants. The empty graph, duplicated adjacency occurrences, self-loops, aliasing among input rows, and arbitrary initial clocks are included.