The trace-formula gap law on the girth window

Let A be the adjacency matrix, B the non-backtracking operator and g the girth of a finite simple graph, and let p_k be the power sums of the roots of its matching polynomial. For 1 ≤ k ≤ g + 1,

tr(Aᵏ) - p_k = tr(Bᵏ).

By Godsil's moment theorem the left side counts the closed walks of length k that are not tree-like. On the window both the non-tree-like closed walks and the closed non-backtracking dart sequences of length k are exactly the rooted traversals of k-cycles, so the two counts agree (at k ∈ {g, g + 1} both are 2k times the number of k-cycles; below the girth both vanish).

Main results

• SimpleGraph.Walk.not_isTreeLike_of_isCycle: a cycle is not tree-like.
• SimpleGraph.Walk.isCycle_of_nbChain_window: on the window a closed non-backtracking walk of positive length is a cycle.
• SimpleGraph.Walk.isCycle_or_isTreeLike_window: on the window a closed walk is a cycle or tree-like.
• SimpleGraph.sum_card_not_treeLike_eq_sum_card_relWalks: the bijection, as an equality of counts.
• SimpleGraph.treeLikeGap_eq_trace_hashimoto: tr(Aᵏ) - treeLikeWalkCount G k = tr(Bᵏ) over ℤ.
• SimpleGraph.trace_sub_matchingPowerSum_eq_trace_hashimoto: tr(Aᵏ) - p_k = tr(Bᵏ) over ℂ.

B-1b: the relWalks membership constructor (converse anatomy)

theorem mem_relWalks_of {V : Type u_1} [Fintype V] [DecidableEq V] {r : V → V → Prop} [DecidableRel r] {k : ℕ} {i j : V} {w : List V} (hlen : w.length = k + 1) (hhead : w.head? = some i) (hlast : w.getLast? = some j) (hch : List.IsChain r w) : w ∈ Matrix.relWalks r k i j

Constructor for relWalks membership: a list of the right length, endpoints and chain is a member. Converse of the anatomy lemmas of NbVanishing.

W1: parity of edge incidences — for ARBITRARY walks

Mathlib's IsTrail.even_countP_edges_iff carries an IsTrail hypothesis that its own proof only uses to feed the induction; the statement is true for every walk. We need the general form: in Lemma B's case |C| = g, k = g+1 the walk is NOT a trail (it may repeat an edge), and the parity of incidences at the extra edge's endpoint is exactly what kills the case.

theorem SimpleGraph.Walk.even_countP_edges_iff' {V : Type u_1} {G : SimpleGraph V} {u v : V} [DecidableEq V] (p : G.Walk u v) (x : V) : Even (List.countP (fun (e : Sym2 V) => decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Parity of edge incidences, general form. For any walk u → v and any vertex x, the number of edge slots incident to x is even iff x avoids the endpoints whenever they are distinct. (Mathlib's version assumes IsTrail; the hypothesis is not needed.)

theorem SimpleGraph.Walk.even_countP_edges_of_closed {V : Type u_1} {G : SimpleGraph V} {u : V} [DecidableEq V] (p : G.Walk u u) (x : V) : Even (List.countP (fun (e : Sym2 V) => decide (x ∈ e)) p.edges)

Closed walks have even incidence everywhere. The parity workhorse for Lemma B.

W2: incidence counts on a cycle

Transfer of IsCycle.ncard_neighborSet_toSubgraph_eq_two from neighbour sets to edge-slot incidence counts: a cycle meets each vertex of its support in exactly two edge slots, and vertices outside the support in none. Together with W1 (parity) this is what bounds the shapes a window walk can take.

theorem SimpleGraph.Walk.countP_edges_eq_zero_of_notMem_support {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u v x : V} {w : G.Walk u v} (hx : x ∉ w.support) : List.countP (fun (e : Sym2 V) => decide (x ∈ e)) w.edges = 0

No edge of a walk is incident to a vertex outside its support.

theorem SimpleGraph.Walk.countP_edges_of_isCycle {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {u x : V} {c : G.Walk u u} (hc : c.IsCycle) (hx : x ∈ c.support) : List.countP (fun (e : Sym2 V) => decide (x ∈ e)) c.edges = 2

W2: a cycle meets each of its support vertices in exactly two edge slots.

B-1c: a cycle is not tree-like

The lift of a cycle extends along its (distinct) support; at the closing step the root v is in the stack but is not the penultimate vertex, so the retreat fails.

theorem SimpleGraph.liftSeq_append_of_nodup {V : Type u_1} [DecidableEq V] (fresh rest stack : List V) (hnd : (stack ++ fresh).Nodup) : liftSeq (fresh ++ rest) stack = liftSeq rest (stack ++ fresh)

Fresh vertices extend the lift stack monotonically: processing a block disjoint from the stack appends it.

theorem SimpleGraph.Walk.not_isTreeLike_of_isCycle {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {c : G.Walk v v} (hc : c.IsCycle) : ¬c.IsTreeLike

B-1c. A cycle is not tree-like.

W3: a closed trail on exactly a cycle's edges is that cycle

If a closed walk's edge list is a permutation of a cycle's edge list, the walk is itself a cycle. The key step: a repeated support vertex x would, after rotating the walk to base x, sit at three pairwise-distinct edge slots {0, m−1, m}; the walk is a trail (its edges are the cycle's, nodup), so these are three DISTINCT edges incident to x — contradicting the exact incidence count 2 of W2.

theorem SimpleGraph.Walk.getVert_mem_edges_getElem {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {t : ℕ} (ht : t < p.length) : p.getVert t ∈ p.edges[t] ∧ p.getVert (t + 1) ∈ p.edges[t]

Both endpoints of the t-th edge slot: getVert t and getVert (t+1) lie in edges[t].

theorem SimpleGraph.Walk.isCycle_of_edges_perm {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v a : V} {w : G.Walk v v} {c : G.Walk a a} (hc : c.IsCycle) (hperm : w.edges.Perm c.edges) (hpos : 0 < w.length) : w.IsCycle

W3. A closed walk of positive length whose edge list is a permutation of a cycle's edge list is itself a cycle.

W4: a closed walk is never "a cycle plus one extra edge slot"

The Lemma B case |C| = g, k = g+1 dies here: if a closed walk's edge multiset were a cycle's edges plus a single extra slot f, then any endpoint x of f would have odd incidence count (2 + 1 if x lies on the cycle, 0 + 1 if not) — contradicting the parity lemma W1. Note: no trail or non-backtracking hypothesis is needed; parity alone kills the case.

theorem SimpleGraph.Walk.not_closed_of_isCycle_edges_add_one {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v a : V} {w : G.Walk v v} {c : G.Walk a a} (hc : c.IsCycle) (hsub : c.edges ⊆ w.edges) (hlen : w.length = c.length + 1) : False

W4. No closed walk has edge multiset = (edges of a cycle) + one extra slot.

B-2: in the window, a closed non-backtracking walk IS a cycle

The composition: the strengthened Lemma A key step extracts a cycle C on the walk's edges with g ≤ |C| ≤ k ≤ g+1, so either |C| = k (W3: the walk is a permutation of the cycle, hence the cycle) or |C| = k−1 (W4: parity kills it).

theorem SimpleGraph.Walk.isCycle_of_nbChain_window {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : G.Walk v v} (hnb : List.IsChain G.nbRel w.darts) (hpos : 0 < w.length) (hwin : ↑w.length ≤ G.egirth + 1) : w.IsCycle

Lemma B-2. A closed non-backtracking walk of positive length at most girth + 1 is a cycle.

B-3: in the window, every closed walk is a cycle or tree-like

No liftSeq induction needed: if the walk is not tree-like its edge-support contains a cycle (isTreeLike_of_acyclic, contrapositive); mapping that cycle into G (edges_map_hom_subset_edges) puts us exactly in the W3/W4 dichotomy — |C| = k makes the walk that cycle, |C| = k−1 is impossible by parity.

theorem SimpleGraph.Walk.isCycle_or_isTreeLike_window {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : G.Walk v v} (hwin : ↑w.length ≤ G.egirth + 1) : w.IsCycle ∨ w.IsTreeLike

B-3. A closed walk of length at most girth + 1 is a cycle or tree-like.

theorem SimpleGraph.Walk.isChain_nbRel_darts_of_isTrail {V : Type u_1} {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsTrail) : List.IsChain G.nbRel w.darts

Trails never backtrack. Consecutive darts of a trail form a non-backtracking chain: a reversal d_{i+1} = d_i.symm would repeat the edge d_i.edge at two distinct positions, contradicting edges_nodup. This gives every cycle (in particular) its NB chain.

B-4: the counting assembly — the Lemma B main theorem

Both sides of the gap law count rooted cycle traversals in the window. The bijection sends a non-tree-like closed walk (= a cycle, by B-3) rooted at a vertex to its dart list closed by the repeat of its first dart (a relWalks G.nbRel member, by B-1a/b + the seam); conversely a member assembles to a cycle (B-2) which is not tree-like (B-1c).

theorem SimpleGraph.Walk.eq_of_darts_eq {V : Type u_1} {G : SimpleGraph V} {u v : V} (p q : G.Walk u v) : p.darts = q.darts → p = q

A walk is determined by its dart list (same endpoints): structural induction, the middle vertex is recovered from the first dart.

theorem SimpleGraph.Walk.isChain_nbRel_concat_of_isCycle {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : G.Walk v v} (hw : w.IsCycle) (hne : w.darts ≠ []) : List.IsChain G.nbRel (w.darts ++ [w.darts.head hne])

The closed non-backtracking chain of a cycle (B-1a + the seam): appending the repeat of the first dart keeps the chain non-backtracking.

theorem SimpleGraph.sum_card_not_treeLike_eq_sum_card_relWalks {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} (hk : 0 < k) (hwin : ↑k ≤ G.egirth + 1) : ∑ v : V, {w ∈ G.finsetWalkLength k v v | ¬w.IsTreeLike}.card = ∑ e : G.Dart, (Matrix.relWalks G.nbRel k e e).card

B-4, the count. In the window, the non-tree-like closed walks and the closed non-backtracking dart walks are equinumerous: both are rooted cycle traversals.

The Lemma B main theorem: the gap law on the full window

theorem SimpleGraph.treeLikeGap_eq_trace_hashimoto {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} (hk : 0 < k) (hwin : ↑k ≤ G.egirth + 1) : treeLikeGap k = (G.hashimoto ℤ ^ k).trace

main theorem. On the whole window 1 ≤ k ≤ girth + 1 the trace-formula gap law holds: tr(Aᵏ) − p_k's combinatorial form equals the Hashimoto trace, treeLikeGap k = tr(Bᵏ). Below the girth both sides vanish (Lemma A); at k ∈ {g, g+1} both count the rooted cycle traversals (2k·c_k).

theorem SimpleGraph.trace_sub_matchingPowerSum_eq_trace_hashimoto {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {k : ℕ} (hk : 0 < k) (hwin : ↑k ≤ G.egirth + 1) : ↑(adjMatrix ℕ G ^ k).trace - matchingPowerSum k = (G.hashimoto ℂ ^ k).trace

The gap law in power-sum form. Composing the main theorem with Godsil's moment theorem (matchingPowerSum_eq_treeLikeWalkCount): on the window 1 ≤ k ≤ girth + 1, tr(Aᵏ) − p_k = tr(Bᵏ) over ℂ, with p_k = Σᵢ θᵢᵏ the power sums of the roots of the matching polynomial. The sharp trace-formula gap law.