Walk reversal and the powered graph

The graph-theoretic half of Dinur's powering step. The t-th power of a regular graph G has the same vertices, and one edge for each walk of length t in G, joining the walk's two ends.

Making that a RegGraph means exhibiting the rotation map: an involution on darts. A dart of the power is a vertex together with a tuple of t labels, and its reverse is the reversed walk — starting at the far end and retracing the same edges backwards. So the work here is to define reversal and prove it is an involution.

How reversal is defined

The k-th dart of the walk (v, s) is (walkAt k, s k); reversing it with G.rot yields the next vertex together with the label that points back, called backLabel. The reversed walk reads those back-labels in reverse order, using Fin.rev — whose own involutivity (Fin.rev_rev) carries most of the index bookkeeping.

rot_dart is the one computational fact everything rests on: reversing the k-th dart gives (walkAt (k+1), backLabel k). Applying G.rot_involutive to it turns each step of the reversed walk back into a step of the original.

Why the power's spectral bound is lam ^ t

The power's walk operator is the t-fold operator of G: averaging over all deg ^ t walks out of a vertex is exactly stepIter t (sum_walkEnd). So the squared-norm contraction of RegularGraph applies verbatim, and a graph with SpectralBound lam powers up to one with SpectralBound (lam ^ t). This is what makes powering amplify the gap.

Main definitions

• RegGraph.backLabel — the label pointing back along a dart of a walk
• RegGraph.revWalk — the reversed walk
• RegGraph.power — the t-th power as a RegGraph

Main results

• RegGraph.rot_dart — reversing the k-th dart of a walk
• RegGraph.walkAt_revWalk — the reversed walk retraces the trajectory
• RegGraph.walkEnd_revWalk, RegGraph.revWalk_revWalk — reversal is an involution
• RegGraph.step_power — the power's walk operator is stepIter t
• RegGraph.spectralBound_power — SpectralBound lam powers to SpectralBound (lam ^ t)
• RegGraph.deg_power, RegGraph.order_power

Reversing the darts of a walk

def Complexity.RegGraph.backLabel (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) (k : Fin t) : G.D

The label at walkAt (k+1) that points back along the k-th dart of the walk (v, s).

Equations

• G.backLabel v s k = (G.rot (G.walkAt t v s ↑k, s k)).2

theorem Complexity.RegGraph.rot_dart (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) (k : Fin t) : G.rot (G.walkAt t v s ↑k, s k) = (G.walkAt t v s (↑k + 1), G.backLabel v s k)

The computational core. Reversing the k-th dart of the walk (v, s) gives the next vertex on the walk, together with the label pointing back.

def Complexity.RegGraph.revWalk (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) : Fin t → G.D

The walk (v, s) reversed: it starts at the far end and reads the back-labels of the original darts in reverse order.

Equations

• G.revWalk v s j = G.backLabel v s j.rev

theorem Complexity.RegGraph.walkAt_revWalk (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) (k : ℕ) : k ≤ t → G.walkAt t (G.walkEnd t v s) (G.revWalk v s) k = G.walkAt t v s (t - k)

The reversed walk retraces the original trajectory backwards.

theorem Complexity.RegGraph.walkEnd_revWalk (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) : G.walkEnd t (G.walkEnd t v s) (G.revWalk v s) = v

Reversing a walk lands back at its start.

theorem Complexity.RegGraph.revWalk_revWalk (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) : G.revWalk (G.walkEnd t v s) (G.revWalk v s) = s

Reversal is an involution on walks.

The powered graph

def Complexity.RegGraph.power (G : RegGraph) (t : ℕ) : RegGraph

The t-th power of G: same vertices, one edge per walk of length t.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegGraph.V_power (G : RegGraph) (t : ℕ) : (G.power t).V = G.V

@[simp]

theorem Complexity.RegGraph.D_power (G : RegGraph) (t : ℕ) : (G.power t).D = (Fin t → G.D)

@[simp]

theorem Complexity.RegGraph.order_power (G : RegGraph) (t : ℕ) : (G.power t).order = G.order

@[simp]

theorem Complexity.RegGraph.deg_power (G : RegGraph) (t : ℕ) : (G.power t).deg = G.deg ^ t

theorem Complexity.RegGraph.nbr_power (G : RegGraph) (t : ℕ) (v : G.V) (s : Fin t → G.D) : (G.power t).nbr v s = G.walkEnd t v s

theorem Complexity.RegGraph.step_power (G : RegGraph) (t : ℕ) (f : G.V → ℝ) (v : G.V) : (G.power t).step f v = G.stepIter t f v

The power's walk operator is the t-fold walk operator of G.

theorem Complexity.RegGraph.spectralBound_power (G : RegGraph) {lam : ℝ} (h : G.SpectralBound lam) (t : ℕ) : (G.power t).SpectralBound (lam ^ t)

Powering amplifies the spectral gap.