Documentation

Formalizations.Combinatorics.SimpleGraph.Ihara.NbVanishing

Non-backtracking traces below the girth #

A closed non-backtracking dart sequence of positive length contains a cycle of the graph of at most its length. Hence tr(Bᵏ) = 0 for 0 < k < g, where g is the girth; below the girth both sides of the trace-formula gap law tr(Aᵏ) - #(tree-like closed walks) = tr(Bᵏ) vanish.

Main results #

Anatomy of relWalks members (generic relation) #

source
theorem isChain_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 ∈ Matrix.relWalks r k i j) :
List.IsChain r w

Every walk in relWalks r k i j is an r-chain.

source
theorem getLast?_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 ∈ Matrix.relWalks r k i j) :
w.getLast? = some j

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

source
theorem length_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 ∈ Matrix.relWalks r k i j) :
w.length = k + 1

Every walk in relWalks r k i j visits k + 1 vertices.

Dart-list anatomy of short walks #

source
theorem SimpleGraph.Walk.darts_eq_singleton_of_length_eq_one {V : Type u_1} {G : SimpleGraph V} {x y : V} {q : G.Walk x y} (hq : q.length = 1) :
∃ (hadj : G.Adj x y), q.darts = [{ fst := x, snd := y, adj := hadj }]

A walk of length one consists of a single dart joining its endpoints.

The key step: a non-backtracking chain with a repeated vertex contains a cycle #

source
theorem SimpleGraph.Walk.exists_isCycle_of_nbChain_of_not_nodup {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v : V} (w : G.Walk u v) (hnb : List.IsChain G.nbRel w.darts) (hdup : ¬w.support.Nodup) :
∃ (a : V) (c : G.Walk a a), c.IsCycle ∧ c.length ≤ w.length ∧ c.edges ⊆ w.edges

The cycle-extraction key step. A walk whose darts form a non-backtracking chain (Chain' G.nbRel) and whose support repeats a vertex contains a cycle of length at most the walk's length, supported on the walk's own edges. Structural induction; the takeUntil prefix of a nodup support is a path, so the only obstruction to closing the cycle — the closing edge already lying on the path — forces an immediate backtrack, contradicting the chain.

Assembly: emptiness, vanishing trace, and the below-girth gap law #

The dart-list → walk assembly is Mathlib's Walk.ofDarts on the FULL member list: the last dart repeats the first, so the walk's support repeats a vertex (key step applies) and its edge list has at most k distinct entries (pigeonhole bounds the extracted cycle below g).

source
theorem SimpleGraph.relWalks_nbRel_closed_eq_empty {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} (hk : 0 < k) (hg : ↑k < G.egirth) (e : G.Dart) :
Matrix.relWalks G.nbRel k e e = ∅

No closed non-backtracking walk below the girth.

source
theorem SimpleGraph.trace_hashimoto_pow_eq_zero_of_lt_egirth {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (R : Type u_2) [CommRing R] {k : ℕ} (hk : 0 < k) (hg : ↑k < G.egirth) :
(G.hashimoto R ^ k).trace = 0

Lemma A, non-backtracking side. Below the girth the Hashimoto traces vanish: tr(Bᵏ) = 0 for 1 ≤ k < g.

source
theorem SimpleGraph.treeLikeGap_eq_trace_hashimoto_of_lt_egirth {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} (hk : 0 < k) (hg : ↑k < G.egirth) :
treeLikeGap k = (G.hashimoto ℤ ^ k).trace

Lemma A: the gap law below the girth. For 1 ≤ k < g both sides of the trace-formula gap law vanish, so gap_k = tr(Bᵏ) holds (trivially) on the whole below-girth range. The remaining window k ∈ {g, g+1} (where both sides equal 2k·c_k) is Lemma B.