Internal helpers for Valiant's Depth Reduction Lemma

Proof machinery supporting Valiant.depth_reduction. The public statement and high-level wrapper live in Circ.Valiant; the basic digraph definitions used below — IsDirectedPath, IsSimplePath, depth, edgeFinset, deleteEdges — live in Circ.Digraph.Defs. This file defines the canonical labeling and collects the canonical labeling argument, the edge partition by first-differing bit, the averaging step, and the relabeling-after-removal bound.

noncomputable def Digraph.canonicalLabel {V : Type u_1} [Fintype V] (G : Digraph V) (v : V) : ℕ

The canonical labeling of G: the length — node count — of a longest simple directed path ending at v. Parameterized by edge count n, with the outer + 1 converting to node count; the single-vertex path ![v] always witnesses n = 0, so the label is automatically at least 1.

Equations

• G.canonicalLabel v = sSup {n : ℕ | ∃ (p : Fin (n + 1) → V), G.IsSimplePath p ∧ p (Fin.last n) = v} + 1

Acyclicity and legal labelings

def CircuitComplexity.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

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

theorem CircuitComplexity.Valiant.one_le_canonicalLabel {V : Type u_1} [Fintype V] (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 CircuitComplexity.Valiant.canonicalLabel_le_depth {V : Type u_1} [Fintype V] (G : Digraph V) (hac : G.IsAcyclic) (v : V) : G.canonicalLabel v ≤ G.depth

In an acyclic digraph, the canonical label is bounded above by the graph's depth. (In a cyclic digraph the canonical label can exceed the walk-supremum depth = 0, so acyclicity is needed.)

theorem CircuitComplexity.Valiant.canonicalLabel_isLegal {V : Type u_1} [Fintype 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 CircuitComplexity.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 CircuitComplexity.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

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

noncomputable def CircuitComplexity.Valiant.levelEdges {V : Type u_1} [Fintype V] [DecidableEq 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

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

theorem CircuitComplexity.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 CircuitComplexity.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 CircuitComplexity.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.