Tree-like walk counts and matching power sums

Godsil's moment theorem states that the power sums p_k = ∑ᵢ θᵢᵏ of the roots of the matching polynomial count the closed tree-like walks of length k. This file defines both sides and the gap tr(Aᵏ) - #(closed tree-like walks), and proves that below the girth every closed walk is tree-like, so the gap vanishes there.

Main definitions

• SimpleGraph.treeLikeWalkCount G k: the number of closed tree-like walks of length k.
• SimpleGraph.matchingPowerSum G k: ∑ θᵏ over the complex roots θ of μ(G).
• SimpleGraph.treeLikeGap G k: tr(Aᵏ) - treeLikeWalkCount G k.

Main results

• SimpleGraph.Walk.isTreeLike_of_length_lt_egirth: closed walks shorter than the girth are tree-like.
• SimpleGraph.treeLikeWalkCount_eq_trace_of_lt_egirth, SimpleGraph.treeLikeGap_eq_zero_of_lt_egirth.
• SimpleGraph.treeLikeGap_eq_card_not_treeLike: the gap counts the closed walks that are not tree-like.

References

• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.

The tree-like predicate Walk.IsTreeLike (path-tree-faithful: a closed walk lifts to a closed walk at the root of Godsil's path tree T(G,v)) is defined in PathTreeLift, with its Decidable instance, nil_isTreeLike, and isTreeLike_of_acyclic (acyclic edge-support ⇒ tree-like). Below the girth that hypothesis always holds (acyclic_of_length_lt_egirth, below), so the two notions coincide there; the path-tree definition is the one matching the matching power sums p_k for all k (e.g. K4, k = 6 → 324, where the bare acyclic-support count gives 276).

theorem SimpleGraph.Walk.edges_map_hom_subset_edges {V : Type u_1} {G : SimpleGraph V} {v : V} (w : G.Walk v v) {u : ↑w.toSubgraph.verts} (c : w.toSubgraph.coe.Walk u u) : (Walk.map w.toSubgraph.hom c).edges ⊆ w.edges

The edges of a walk in the coerced support w.toSubgraph.coe, pushed into G, all lie among the edges of w itself: the mapped walk's support is contained in w.toSubgraph.

theorem SimpleGraph.Walk.acyclic_of_length_lt_egirth {V : Type u_1} {G : SimpleGraph V} {v : V} (w : G.Walk v v) (h : ↑w.length < G.egirth) : w.toSubgraph.coe.IsAcyclic

Girth threshold (acyclic form). A closed walk strictly shorter than the (extended) girth has acyclic edge-support: any cycle in its support lifts to a cycle of G no longer than the walk, contradicting the girth bound. (For an acyclic G, egirth = ⊤, so this holds for every closed walk.)

theorem SimpleGraph.Walk.isTreeLike_of_length_lt_egirth {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {v : V} (w : G.Walk v v) (h : ↑w.length < G.egirth) : w.IsTreeLike

Girth threshold. A closed walk strictly shorter than the (extended) girth is tree-like: below the girth the edge-support is acyclic (acyclic_of_length_lt_egirth), and an acyclic support lifts to the path tree (isTreeLike_of_acyclic, PathTreeLift).

Below the girth: tree-like walks are all closed walks (tr(Aᵏ) counts them)

theorem SimpleGraph.card_filter_isTreeLike_of_lt_egirth {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {k : ℕ} {v : V} (h : ↑k < G.egirth) : {w ∈ G.finsetWalkLength k v v | w.IsTreeLike}.card = (G.finsetWalkLength k v v).card

Below the (extended) girth, every closed walk of length k is tree-like, so filtering the closed walks of length k by IsTreeLike keeps all of them.

theorem SimpleGraph.trace_adjMatrix_pow_eq_treeLike_of_lt_egirth {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) (h : ↑k < G.egirth) : (adjMatrix ℕ G ^ k).trace = ∑ v : V, {w ∈ G.finsetWalkLength k v v | w.IsTreeLike}.card

Below the girth, tr(Aᵏ) counts closed tree-like walks. Combining piece 1 of the trace formula (trace_adjMatrix_pow, tr(Aᵏ) = #closed walks) with the girth threshold: for k < girth, every closed walk is tree-like, so tr(Aᵏ) = Σ_v #{closed tree-like walks of length k at v}. This is the gap_k = 0 half of the matching↔Ihara main (tr(Aᵏ) = p_k below girth, once Godsil's p_k = #tree-like walks lands).

The matching side: Godsil's tree-like walk count

Godsil's moment theorem (proved in MomentAssembly) reads

p_k = Σᵢ θᵢᵏ = treeLikeWalkCount G k,

where θᵢ are the roots of matchingPoly G and treeLikeWalkCount is defined below.

noncomputable def SimpleGraph.treeLikeWalkCount {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) : ℕ

Godsil's tree-like walk count Σ_v #{closed tree-like walks of length k at v} — the matching side of the trace-formula bridge.

Equations

• SimpleGraph.treeLikeWalkCount k = ∑ v : V, {w ∈ G.finsetWalkLength k v v | w.IsTreeLike}.card

theorem SimpleGraph.treeLikeWalkCount_eq_trace_of_lt_egirth {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) (h : ↑k < G.egirth) : treeLikeWalkCount k = (adjMatrix ℕ G ^ k).trace

Trace link (below girth). For k < girth, treeLikeWalkCount G k = tr(Aᵏ), since below the girth every closed walk is tree-like. The proved half of the bridge: combined with Godsil's (open) p_k = treeLikeWalkCount, it yields p_k = tr(Aᵏ) below the girth.

theorem SimpleGraph.treeLikeWalkCount_zero {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] : treeLikeWalkCount 0 = Fintype.card V

k = 0 moment anchor: treeLikeWalkCount G 0 = n. The only closed walk of length 0 at each vertex is nil (tree-like), so the count is 1 per vertex. This is the matching-side mirror of the trivial power sum p_0 = Σᵢ θᵢ⁰ = n (μ has n roots).

The matching-side power sums p_k (the other half of the bridge)

noncomputable def SimpleGraph.matchingPowerSum {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) : ℂ

Matching-side power sum p_k = Σᵢ θᵢᵏ over the (complex) roots of the matching polynomial. Godsil's moment theorem is the (open) bridge matchingPowerSum G k = treeLikeWalkCount G k.

Equations

• SimpleGraph.matchingPowerSum k = (Multiset.map (fun (x : ℂ) => x ^ k) (Polynomial.map (algebraMap ℝ ℂ) G.matchingPoly).roots).sum

theorem SimpleGraph.matchingPowerSum_zero {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] : matchingPowerSum 0 = ↑(Fintype.card V)

k = 0 anchor: matchingPowerSum G 0 = n. The matching polynomial is monic of degree n = card V, so over the algebraically closed ℂ it splits into exactly n linear factors, i.e. its multiset of roots has cardinality n; each root contributes θ⁰ = 1 to the power sum. Together with treeLikeWalkCount_zero this confirms Godsil's bridge matchingPowerSum = treeLikeWalkCount at k = 0 on both sides.

The trace-formula gap

treeLikeGap G k := tr(Aᵏ) − treeLikeWalkCount G k counts the closed walks of length k that are not tree-like — those whose edge-support encloses a cycle. It vanishes below the girth (treeLikeGap_eq_zero_of_lt_egirth, proved here). At k = girth it takes the value

treeLikeGap G g = 2·g·c_g, c_g = number of cycles of length g = girth,

since the only closed walks of length g enclosing a cycle are the single traversals of a shortest cycle (2g per cycle: g starting points × 2 orientations).

noncomputable def SimpleGraph.treeLikeGap {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) : ℤ

Trace-formula gap tr(Aᵏ) − treeLikeWalkCount G k: the count of closed length-k walks that are not tree-like (they enclose a cycle).

Equations

• SimpleGraph.treeLikeGap k = ↑(SimpleGraph.adjMatrix ℕ G ^ k).trace - ↑(SimpleGraph.treeLikeWalkCount k)

theorem SimpleGraph.treeLikeGap_eq_zero_of_lt_egirth {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) (h : ↑k < G.egirth) : treeLikeGap k = 0

The gap vanishes below the girth. Every closed walk shorter than the girth is tree-like, so tr(Aᵏ) = treeLikeWalkCount G k there. The first nonzero gap appears exactly at k = girth (value 2·girth·c_g, classical, not yet formalized).

theorem SimpleGraph.treeLikeGap_eq_card_not_treeLike {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] (k : ℕ) : treeLikeGap k = ∑ v : V, ↑{w ∈ G.finsetWalkLength k v v | ¬w.IsTreeLike}.card

The gap counts the non-tree-like closed walks (bijection, piece 1): treeLikeGap G k = Σ_v #{closed length-k walks at v that are not tree-like}. Immediate from tr(Aᵏ) = Σ_v #(all) and treeLikeWalkCount = Σ_v #(tree-like), since all = tree-like ⊔ not-tree-like.