Internal helpers for Valiant's Depth Reduction Lemma

Proof machinery supporting Valiant.depth_reduction. The public statement and high-level wrapper live in Complexitylib.Circuits.Valiant; the basic digraph definitions used below — IsDirectedWalk, IsPath, canonicalLabel, depth, edgeFinset, deleteEdges — live in Complexitylib.Mathlib.Digraph. This file collects the canonical labeling argument (legality and depth bounds for canonicalLabel), the edge partition by first-differing bit, the averaging step, and the relabeling-after-removal bound.

Acyclicity and legal labelings

def Complexity.Valiant.IsLegalLabeling {V : Type u_1} (G : Digraph V) (ℓ : V → ℕ) : Prop

A legal labeling of a digraph is a map to the naturals that is strictly increasing along every edge.

Equations

• Complexity.Valiant.IsLegalLabeling G ℓ = ∀ (u v : V), G.Adj u v → ℓ u < ℓ v

theorem Complexity.Valiant.one_le_canonicalLabel {V : Type u_1} (G : Digraph V) (v : V) : 1 ≤ G.canonicalLabel v

Every canonical label is at least 1: immediate from the outer + 1 in the definition.

theorem Complexity.Valiant.canonicalLabel_le_depth {V : Type u_1} [Fintype V] (G : Digraph V) (v : V) : G.canonicalLabel v ≤ G.depth

The canonical label is bounded above by the graph's simple-path depth.

theorem Complexity.Valiant.canonicalLabel_isLegal {V : Type u_1} [Fintype V] [DecidableEq V] (G : Digraph V) (hac : G.IsAcyclic) : IsLegalLabeling G G.canonicalLabel

Canonical labeling is legal in acyclic graphs. Any simple path ending at u followed by the edge (u,v) is a strictly longer simple path ending at v (using acyclicity to ensure v does not already appear in the path).

theorem Complexity.Valiant.depth_le_image_card {V : Type u_1} [Fintype V] (G : Digraph V) {ℓ : V → ℕ} (hℓ : IsLegalLabeling G ℓ) : G.depth ≤ (Finset.image ℓ Finset.univ).card

Depth bound from a legal labeling. Along any directed path, labels are strictly increasing, hence distinct. So depth(G) is at most the number of distinct labels used by any legal labeling.

Partitioning edges by first-differing bit

Under IsAcyclic G and G.depth ≤ 2 ^ k, each canonical label G.canonicalLabel v lies in {1,...,2^k}, so after subtracting 1 its k-bit binary representation is well-defined. For each edge (u,v), since canonical labels are strictly increasing, the k-bit reps of ℓ(u)-1 and ℓ(v)-1 differ, and we can identify the leftmost (MSB) bit at which they first disagree.

def Complexity.Valiant.firstDifferBit (k a b : ℕ) : ℕ

firstDifferBit k a b is the 1-indexed MSB position at which the k-bit binary representations of a and b first disagree, or 0 if the two k-bit representations coincide. The MSB of a XOR b (as indexed by Nat.log2 from the LSB) gives the position of first difference; converting to 1-indexed-from-MSB gives k - Nat.log2.

Equations

• Complexity.Valiant.firstDifferBit k a b = if a = b then 0 else k - (a ^^^ b).log2

noncomputable def Complexity.Valiant.levelEdges {V : Type u_1} [Fintype V] (G : Digraph V) [DecidableRel G.Adj] (k i : ℕ) : Finset (V × V)

Edges whose canonical-label endpoints' k-bit binary representations first disagree at MSB position i.

Equations

• Complexity.Valiant.levelEdges G k i = {e ∈ G.edgeFinset | Complexity.Valiant.firstDifferBit k (G.canonicalLabel e.1 - 1) (G.canonicalLabel e.2 - 1) = i}

theorem Complexity.Valiant.sum_card_levelEdges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj] {k : ℕ} (hac : G.IsAcyclic) (hd : G.depth ≤ 2 ^ k) : ∑ i ∈ Finset.Ioc 0 k, (levelEdges G k i).card = G.edgeFinset.card

Partition. When G is acyclic and G.depth ≤ 2 ^ k, every edge lies in exactly one level E_i for i ∈ {1,...,k}.

theorem Complexity.Valiant.exists_r_levels_small {V : Type u_1} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj] {k r : ℕ} (hrk : r ≤ k) (hac : G.IsAcyclic) (hd : G.depth ≤ 2 ^ k) : ∃ I ⊆ Finset.Ioc 0 k, I.card = r ∧ k * ∑ i ∈ I, (levelEdges G k i).card ≤ r * G.edgeFinset.card

Averaging. There is a choice of r levels whose total edge count is at most r * S / k (equivalently, k * total ≤ r * S).

theorem Complexity.Valiant.depth_deleteEdges_levelEdges_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : Digraph V) [DecidableRel G.Adj] {k : ℕ} (hac : G.IsAcyclic) (hd : G.depth ≤ 2 ^ k) (I : Finset ℕ) (hI : I ⊆ Finset.Ioc 0 k) : (G.deleteEdges (I.biUnion fun (i : ℕ) => levelEdges G k i)).depth ≤ 2 ^ (k - I.card)

Relabeling after removal. After removing the edges in levels I (assuming G acyclic), the map sending each vertex to its canonical label with the I-th bits deleted is a legal labeling of the remaining graph; its image has at most 2 ^ (k - I.card) values, so the remaining depth is bounded by that.