Non-backtracking walks and the Hashimoto operator

The Hashimoto operator is the 0-1 adjacency matrix, cast to R, of the non-backtracking relation on darts (d is followed by e when e starts where d ends and e is not the reversal of d). Hence tr(Bᵏ) counts closed non-backtracking dart sequences of length k.

Main definitions

• SimpleGraph.nbRel: the non-backtracking relation on darts.

Main results

• SimpleGraph.hashimoto_eq_map_relMatrix: B is the cast of Matrix.relMatrix G.nbRel.
• SimpleGraph.trace_hashimoto_pow: tr(Bᵏ) = ∑_e #(closed non-backtracking walks of length k at e).

def SimpleGraph.nbRel {V : Type u_1} (G : SimpleGraph V) (d e : G.Dart) : Prop

The non-backtracking relation on darts: d ⇝ e iff the head of d is the tail of e and e is not the reverse of d. The Hashimoto operator is its 0-1 adjacency matrix.

Equations

• G.nbRel d e = (d.toProd.2 = e.toProd.1 ∧ e ≠ d.symm)

@[instance_reducible]

instance SimpleGraph.instDecidableRelDartNbRel {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) : DecidableRel G.nbRel

Equations

• G.instDecidableRelDartNbRel d e = { decide := decide (d.toProd.2 = e.toProd.1) && decide (e ≠ d.symm), reflects_decide := ⋯ }

theorem SimpleGraph.hashimoto_eq_map_relMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (R : Type u_2) [CommRing R] : G.hashimoto R = (Matrix.relMatrix G.nbRel).map ⇑(Nat.castRingHom R)

The Hashimoto operator over a commutative ring R is the Nat.cast image of the 0-1 adjacency matrix of the non-backtracking relation.

theorem SimpleGraph.trace_hashimoto_pow {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type u_2) [CommRing R] (k : ℕ) : (G.hashimoto R ^ k).trace = ↑(∑ e : G.Dart, (Matrix.relWalks G.nbRel k e e).card)

The Ihara N_k count. The trace of Bᵏ is the natural number of closed non-backtracking walks of length k (summed over the basepoint dart), cast into R. This is the combinatorial identity behind the N_k = tr(Bᵏ) generating function of ihara_Nk_isolated / ihara_Nk_explicit.