Counting and extending non-backtracking walks

This module provides the counting vocabulary for the Alon–Hoory–Linial bound. It builds on IsNonBacktracking, counts walks by their start and end vertices, and describes the one-edge extension operation used in the weighted argument.

Contents

• nb_concat_iff — the extension characterization: a non-nil walk p extended by an edge to t stays non-backtracking iff p was and t differs from p's penultimate vertex. This is the per-step branching rule the count is built on.
• nbWalksFrom — the finset of length-k non-backtracking walks starting at x, bundled with their (varying) endpoints as a sigma type; card_nbWalksFrom identifies its cardinality with the sum over endpoints of the filtered finsetWalkLength.

Formalization note

The bundled count is ∑ v, ((G.finsetWalkLength r x v).filter IsNonBacktracking).card, which equals the cardinality of the sigma-biUnion nbWalksFrom G x r (the endpoints vary, so a bare biUnion over fun v => Finset (G.Walk x v) is not type-correct — the fibers must be tagged by their endpoint first, which is exactly what nbWalksFrom does).

@[instance_reducible]

instance ACMax.decidableIsNonBacktracking {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} : DecidablePred IsNonBacktracking

IsNonBacktracking is decidable: the defining ∀ i, i + 2 ≤ length → … is a bounded quantifier (any witness has i < length), so it reduces to a Nat.decidableBallLT-style decision.

Equations

• ACMax.decidableIsNonBacktracking w = decidable_of_iff (∀ i < w.length, i + 2 ≤ w.length → w.getVert (i + 2) ≠ w.getVert i) ⋯

theorem ACMax.nb_concat_iff {V : Type u_1} {G : SimpleGraph V} {x y t : V} (p : G.Walk x y) (hp : ¬p.Nil) (h : G.Adj y t) : IsNonBacktracking (p.concat h) ↔ IsNonBacktracking p ∧ t ≠ p.penultimate

Extension characterization. A non-nil walk p : G.Walk x y followed by an edge h : Adj y t is non-backtracking iff p is and the new vertex t differs from p's penultimate vertex (so the last step does not reverse the previous one).

def ACMax.sigmaWalkEmb {V : Type u_1} (G : SimpleGraph V) (x v : V) : G.Walk x v ↪ (w : V) × G.Walk x w

The embedding tagging a walk p : G.Walk x v with its endpoint v.

Equations

• ACMax.sigmaWalkEmb G x v = { toFun := fun (p : G.Walk x v) => ⟨v, p⟩, inj' := ⋯ }

def ACMax.nbWalksFrom {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V) (k : ℕ) : Finset ((v : V) × G.Walk x v)

The finset of length-k non-backtracking walks starting at x, bundled with their endpoints.

Equations

• ACMax.nbWalksFrom G x k = Finset.univ.biUnion fun (v : V) => Finset.map (ACMax.sigmaWalkEmb G x v) (Finset.filter ACMax.IsNonBacktracking (G.finsetWalkLength k x v))

theorem ACMax.mem_nbWalksFrom {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {x : V} {k : ℕ} {s : (v : V) × G.Walk x v} : s ∈ nbWalksFrom G x k ↔ s.snd.length = k ∧ IsNonBacktracking s.snd

Membership in nbWalksFrom: a bundled walk lies in it iff it has the right length and is non-backtracking.

theorem ACMax.card_nbWalksFrom {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V) (k : ℕ) : (nbWalksFrom G x k).card = ∑ v : V, (Finset.filter IsNonBacktracking (G.finsetWalkLength k x v)).card

The bundled count equals the sum over endpoints of the filtered finsetWalkLength cardinality.

def ACMax.nbExtend {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V) (s : (v : V) × G.Walk x v) : Finset ((v : V) × G.Walk x v)

The one-edge non-backtracking extensions of a bundled walk s = ⟨u, p⟩: for each neighbour t of u other than the penultimate vertex of p, the walk p.concat _.

Equations

• ACMax.nbExtend G x s = Finset.image (fun (t : V) => if h : G.Adj s.fst t then ⟨t, s.snd.concat h⟩ else ⟨x, SimpleGraph.Walk.nil⟩) (G.neighborFinset s.fst \ {s.snd.penultimate})