Undirected connectivity by short walks in an explicit graph

This is the combinatorial core of Reingold's theorem that undirected s–t connectivity is in deterministic logarithmic space Reingold, Theorem 4.1 Arora and Barak, Section 21.4, with explicit constants. For a simple graph G on Fin n and any a with n ≤ 2 ^ a:

1. the slot graph of G (Cslib.RotationMap.slotGraph, with the slots of a vertex in the cyclic order of finRotate n) is a 3-regular multigraph on Fin n × Fin n with the connectivity of G; its labels are extended by self-loops to the 257 ^ 8 vertices of the base graph below, so that at least half of the edges at every vertex are self-loops (Cslib.Reachability.Reingold.input);
2. the base graph Cslib.Reachability.Reingold.base is the arithmetic zig-zag base graph over ZMod 257 (Cslib.RotationMap.affinePlaneTowerBase), a 257 ^ 2-regular multigraph on 257 ^ 8 vertices of spectral expansion at most 1 / 5, computed by field arithmetic;
3. depth a = 16 a + 524 steps of Reingold's transformation (Cslib.RotationMap.reingold) make every connected component an expander with λ ≤ 4 / 5, and walks of length walkLength a = 4 (2 a + 65 depth a) reach every vertex of a component.

So t is reachable from s exactly when some walk of length walkLength a in graph G a from the vertex start s a over the slot (s, s) ends over a slot of t (Cslib.Reachability.Reingold.reachable_iff_exists_walk_of_le_two_pow), and with a = ⌈log₂ n⌉ (Cslib.Reachability.Reingold.reachable_iff_exists_walk). Both the depth and the walk length are O(log n), and the graph has constant degree 257 ^ 8, so the walks can be enumerated with O(log n) bits.

The constants are far from optimal: they come from the gap growth γ ↦ min (6 γ / 5) (1 / 5) of a step that squares once (Cslib.RotationMap.min_le_one_sub_spectralExpansion_reingoldStep), from the initial gap 1 / (2 N² |B|²) given by Cheeger's inequality, and from rounding log₂ (6 / 5) and log₂ (5 / 4) down to 1 / 4.

Main definitions

• Cslib.Reachability.Reingold.Label, Cslib.Reachability.Reingold.base: the labels and the base graph.
• Cslib.Reachability.Reingold.input: the regular rotation map of a simple graph on Fin n.
• Cslib.Reachability.Reingold.depth, Cslib.Reachability.Reingold.walkLength: the number of steps of the transformation and the walk length.
• Cslib.Reachability.Reingold.graph, Cslib.Reachability.Reingold.start: the transformed graph and the start vertex over s.

Main results

• Cslib.Reachability.Reingold.spectralExpansion_base_le: the base graph has λ ≤ 1 / 5.
• Cslib.Reachability.Reingold.reachable_input_iff: the regular rotation map has the connectivity of the simple graph.
• Cslib.Reachability.Reingold.reachable_iff_exists_walk_of_le_two_pow, Cslib.Reachability.Reingold.reachable_iff_exists_walk: undirected connectivity is decided by the walks of length O(log n) from one vertex of the constant-degree graph graph G a.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

@[reducible, inline]

abbrev Cslib.Reachability.Reingold.Label : Type

The labels of the graphs of Reingold's transformation: the 257 ^ 8 vertices of the base graph, eight coordinates in ZMod 257.

@[reducible, inline]

abbrev Cslib.Reachability.Reingold.BaseLabel : Type

The labels of the base graph: pairs of elements of ZMod 257.

def Cslib.Reachability.Reingold.base : RotationMap Label BaseLabel

The base graph of the transformation: the arithmetic zig-zag base graph over ZMod 257, a 257 ^ 2-regular multigraph on 257 ^ 8 vertices.

def Cslib.Reachability.Reingold.baseEquiv : Label ≃ (Fin 2 → BaseLabel × BaseLabel)

The vertices of the base graph name the pairs of pairs of its labels.

theorem Cslib.Reachability.Reingold.card_label : Fintype.card Label = 257 ^ 8

There are 257 ^ 8 labels.

theorem Cslib.Reachability.Reingold.spectralExpansion_base_le : base.spectralExpansion ≤ 1 / 5

The base graph is a good expander: its spectral expansion is at most 1 / 5.

def Cslib.Reachability.Reingold.slotLabel : RotationMap.SlotLabel ↪ Label

The three labels of the slot graph, as labels of the base graph.

def Cslib.Reachability.Reingold.input {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : RotationMap (Fin n × Fin n) Label

The regular rotation map of a simple graph on Fin n: its slot graph, with the slots of a vertex in the cyclic order of finRotate n, with self-loops added to reach the labels of the base graph.

theorem Cslib.Reachability.Reingold.reachable_input_iff {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {p q : Fin n × Fin n} : (input G).toSimpleGraph.Reachable p q ↔ G.Reachable p.1 q.1

The regular rotation map has the connectivity of the simple graph: a slot q is reachable from a slot p exactly when the vertex of q is reachable from the vertex of p in G.

theorem Cslib.Reachability.Reingold.card_le_two_mul_card_filter_neighbor_input_eq {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (v : Fin n × Fin n) : Fintype.card Label ≤ 2 * {b : Label | (input G).neighbor v b = v}.card

At least half of the edges at every vertex of the regular rotation map are self-loops.

def Cslib.Reachability.Reingold.depth (a : ℕ) : ℕ

The number of steps of the transformation for graphs on at most 2 ^ a vertices: 16 a + 524.

def Cslib.Reachability.Reingold.walkLength (a : ℕ) : ℕ

The length of the walks for graphs on at most 2 ^ a vertices: 4 (2 a + 65 depth a).

def Cslib.Reachability.Reingold.graph {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (a : ℕ) : RotationMap (RotationMap.ReingoldVertex (Fin n × Fin n) Label (depth a)) Label

Reingold's graph of a simple graph on Fin n: depth a steps of Reingold's transformation applied to its regular rotation map, a 257 ^ 8-regular multigraph.

def Cslib.Reachability.Reingold.start {n : ℕ} (s : Fin n) (a : ℕ) : RotationMap.ReingoldVertex (Fin n × Fin n) Label (depth a)

The start vertex of the walks from s: the vertex (⋯ ((s, s), 0) ⋯, 0) of Reingold's graph, over the slot (s, s).

theorem Cslib.Reachability.Reingold.reachable_iff_exists_walk_of_le_two_pow {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] {a : ℕ} (ha : n ≤ 2 ^ a) (s t : Fin n) : G.Reachable s t ↔ ∃ (k : Fin (walkLength a) → Label), (((graph G a).pow (walkLength a)).neighbor (start s a) k).root.1 = t

Undirected connectivity by short walks in Reingold's graph, the combinatorial part of the proof of Reingold, Theorem 4.1 Arora and Barak, Section 21.4: for a simple graph G on Fin n with n ≤ 2 ^ a, t is reachable from s exactly when some walk of length walkLength a in the 257 ^ 8-regular graph graph G a from start s a ends at a vertex over a slot (t, w) of t.

theorem Cslib.Reachability.Reingold.reachable_iff_exists_walk {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (s t : Fin n) : G.Reachable s t ↔ ∃ (k : Fin (walkLength (Nat.clog 2 n)) → Label), (((graph G (Nat.clog 2 n)).pow (walkLength (Nat.clog 2 n))).neighbor (start s (Nat.clog 2 n)) k).root.1 = t

Undirected connectivity by short walks in Reingold's graph, with a = ⌈log₂ n⌉: t is reachable from s exactly when some walk of length walkLength ⌈log₂ n⌉ = O(log n) in the 257 ^ 8-regular graph graph G ⌈log₂ n⌉ from start s ⌈log₂ n⌉ ends over a slot of t.