Walk counting for a finite digraph (the power of a 0-1 matrix)

For a decidable relation r on a finite type V (a finite directed graph) we count directed walks by powers of its 0-1 adjacency matrix. This is the directed-graph analogue of SimpleGraph.adjMatrix_pow_apply_eq_card_walk, which Mathlib provides for simple graphs. The file also expresses trace (Mᵏ) as a sum over closed index sequences and proves its invariance under cyclic rotation.

Main definitions

• Matrix.relMatrix r: the ℕ-valued 0-1 adjacency matrix of r.
• Matrix.relWalks r k i j: the finset of length-k directed r-walks from i to j, as vertex lists.

Main results

• Matrix.relMatrix_pow_apply: ((relMatrix r) ^ k) i j = (relWalks r k i j).card.
• Matrix.pow_apply_eq_sum, Matrix.trace_pow_eq_sum_closed: entries and trace of Mᵏ as sums over index sequences.
• Matrix.trace_pow_eq_sum_cyclicProd: the same sum written with cyclic products, which are invariant under rotation (Matrix.cyclicProd_comp_finRotate).

def Matrix.relMatrix {V : Type u_1} (r : V → V → Prop) [DecidableRel r] : Matrix V V ℕ

The ℕ-valued 0-1 adjacency matrix of a decidable relation r.

Equations

• Matrix.relMatrix r i j = if r i j then 1 else 0

def Matrix.relWalks {V : Type u_1} [Fintype V] [DecidableEq V] (r : V → V → Prop) [DecidableRel r] : ℕ → V → V → Finset (List V)

The finset of length-k directed r-walks from i to j, encoded as the list of visited vertices [i, …, j].

Equations

• Matrix.relWalks r 0 x✝¹ x✝ = if x✝¹ = x✝ then {[x✝¹]} else ∅
• Matrix.relWalks r k.succ x✝¹ x✝ = Finset.univ.biUnion fun (l : V) => if r x✝¹ l then Finset.map { toFun := List.cons x✝¹, inj' := ⋯ } (Matrix.relWalks r k l x✝) else ∅

theorem Matrix.pow_apply_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] {R : Type u_2} [CommSemiring R] (M : Matrix V V R) (k : ℕ) (i j : V) : (M ^ k) i j = ∑ p : Fin (k + 1) → V, if p 0 = i ∧ p (Fin.last k) = j then ∏ t : Fin k, M (p t.castSucc) (p t.succ) else 0

The (i, j) entry of Mᵏ as a sum, over length-k vertex walks i → j (encoded as Fin (k+1) → V tuples with fixed endpoints), of the product of the edge weights.

theorem Matrix.trace_pow_eq_sum_closed {V : Type u_1} [Fintype V] [DecidableEq V] {R : Type u_2} [CommSemiring R] (M : Matrix V V R) (k : ℕ) : (M ^ k).trace = ∑ p : Fin (k + 1) → V, if p 0 = p (Fin.last k) then ∏ t : Fin k, M (p t.castSucc) (p t.succ) else 0

The trace of Mᵏ counts closed walks. It is the sum, over closed length-k walks (tuples p : Fin (k+1) → V with p 0 = p (last)), of the product of the edge weights.

Rotation invariance — toward closed geodesics

def Matrix.cyclicProd {V : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} (M : Matrix V V R) (w : Fin (n + 1) → V) : R

The cyclic product of edge weights along a closed walk w : Fin (n+1) → V, ∏ₜ M (w t) (w (σ t)) where σ = finRotate (n+1) is the cyclic successor.

Equations

• M.cyclicProd w = ∏ t : Fin (n + 1), M (w t) (w ((finRotate (n + 1)) t))

theorem Matrix.cyclicProd_comp_finRotate {V : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} (M : Matrix V V R) (w : Fin (n + 1) → V) : M.cyclicProd (w ∘ ⇑(finRotate (n + 1))) = M.cyclicProd w

Rotation invariance. The cyclic product is unchanged when the closed walk is rotated by the cyclic shift finRotate. This is what makes the weight a class function on rotation orbits — the structure that groups closed non-backtracking walks into (prime) geodesics.

theorem Matrix.cyclicProd_comp_finRotate_iterate {V : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} (M : Matrix V V R) (w : Fin (n + 1) → V) (j : ℕ) : M.cyclicProd (w ∘ (⇑(finRotate (n + 1)))^[j]) = M.cyclicProd w

Invariance under the whole rotation group. The cyclic product is unchanged by any iterate of finRotate — i.e. it is a class function on the ℤ/(n+1) rotation orbits.

theorem Matrix.trace_pow_eq_sum_cyclicProd {V : Type u_1} [Fintype V] [DecidableEq V] {R : Type u_2} [CommSemiring R] {m : ℕ} (M : Matrix V V R) : (M ^ (m + 1)).trace = ∑ w : Fin (m + 1) → V, M.cyclicProd w

The cyclic trace formula. tr(M^(m+1)) is the sum, over all closed cyclic walks w : Fin (m+1) → V, of the cyclic product of edge weights. Connects the closed-walk trace (trace_pow_eq_sum_closed) to the rotation-equivariant cyclicProd.

theorem Matrix.head?_of_mem_relWalks {V : Type u_1} [Fintype V] [DecidableEq V] {r : V → V → Prop} [DecidableRel r] {k : ℕ} {i j : V} {w : List V} (hw : w ∈ relWalks r k i j) : w.head? = some i

Every walk in relWalks r k i j starts at i.

theorem Matrix.relMatrix_pow_apply {V : Type u_1} [Fintype V] [DecidableEq V] {r : V → V → Prop} [DecidableRel r] (k : ℕ) (i j : V) : (relMatrix r ^ k) i j = (relWalks r k i j).card

Powers of the 0-1 adjacency matrix count directed walks.