Valiant's Depth Reduction Lemma

The length of a directed path is the number of nodes in it. The depth of a directed graph is the length of a longest directed walk.

Lemma (Valiant, 1977). In any directed graph with S edges and depth d = 2 ^ k, for any 1 ≤ r ≤ k, it is possible to remove r * S / k edges so that the depth of the resulting graph does not exceed d / 2 ^ r.

Reference: L. G. Valiant, Graph-theoretic arguments in low-level complexity, MFCS 1977. Stated as Lemma 1.4 in Jukna, Boolean Function Complexity.

Note on cycles: depth is defined here as the supremum (in ℕ) of walk lengths, with no injectivity requirement on the walk. In the presence of a directed cycle, walks can be made arbitrarily long, so the supremum's underlying set is unbounded; by ℕ's convention this gives depth = 0. Consequently, G.depth ≤ 2 ^ k is satisfied trivially (with F = ∅) for cyclic graphs, and is the meaningful bound only on acyclic graphs — the case where Jukna's labeling argument proceeds.

The proof machinery — canonical labelings, the edge partition by first-differing bit, averaging, and the relabeling-after-removal bound — lives in Circ.Internal.Valiant.

theorem CircuitComplexity.Valiant.depth_reduction {V : Type u_1} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj] {k r : ℕ} (hrk : r ≤ k) (hd : G.depth ≤ 2 ^ k) : ∃ F ⊆ G.edgeFinset, k * F.card ≤ r * G.edgeFinset.card ∧ (G.deleteEdges F).depth ≤ 2 ^ k / 2 ^ r

Valiant's Depth Reduction Lemma (Valiant, 1977).

In any finite directed graph G with S edges and depth at most 2 ^ k, for any r ≤ k, there exists a set F of edges such that:

• F is a subset of the edge set,
• k * F.card ≤ r * S (equivalent to |F| ≤ r * S / k without integer division), and
• after removing F, the resulting digraph has depth at most 2 ^ k / 2 ^ r.

For cyclic G the hypothesis is satisfied trivially (with depth = 0) and the conclusion holds with F = ∅. The substantive content is the acyclic case, handled via Jukna's canonical labeling argument.