Godsil's moment theorem

The power sums p_k = ∑ᵢ θᵢᵏ of the roots of the matching polynomial count the closed tree-like walks: p_k = treeLikeWalkCount G k for every k.

The generating function of the tree-like walk counts is the sum over v of the root resolvents of the path trees T(G, v); by Godsil's identity each root resolvent is a ratio of reversed matching polynomials, and the vertex-deletion derivative law turns the sum into reverse(X μ'(G)) divided by reverse μ(G). The generating function of the power sums is the same ratio, and cancelling the unit reverse μ(G) in ℂ⟦X⟧ gives the equality of coefficients.

Main results

• Polynomial.mk_powerSum_mul_reverse: the power-sum generating function of a monic p over ℂ times reverse p is reflect (X p').
• SimpleGraph.resolventSeries_pathTree_mul_reverse_matchingPoly: the root resolvent of T(G, v) times reverse μ(T(G, v)).
• SimpleGraph.mk_treeLikeWalkCount_mul_reverse_eq, SimpleGraph.mk_matchingPowerSum_mul_reverse_eq.
• SimpleGraph.matchingPowerSum_eq_treeLikeWalkCount: Godsil's moment theorem.

References

• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.
• C. D. Godsil, Algebraic Combinatorics, Chapman & Hall, 1993, Chapter 6.

theorem Matrix.det_eq_det_submatrix_ne_of_row_eq_single {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (B : Matrix n n R) (i : n) (hrow : B i = Pi.single i 1) : B.det = (B.submatrix Subtype.val Subtype.val).det

(GL) Determinant collapses to a principal minor when a row is a basis vector. If row i of B is eᵢ = Pi.single i 1, then det B = det (B∖i) (the {j ≠ i} principal minor). Block-triangular reindex n ≃ {·=i} ⊕ {·≠i} (Equiv.sumCompl): row i being eᵢ kills the top-right block, so det_fromBlocks_zero₁₂ factors the determinant as (1×1 block = 1) · det(B∖i). This is the matrix-with-an-isolated-index determinant, the abstraction of adjugate_apply_self_eq_det_submatrix.

theorem Polynomial.sum_reverse_eq_reflect_sum {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (p : ι → Polynomial R) (N : ℕ) (hp : ∀ i ∈ s, (p i).natDegree = N) : ∑ i ∈ s, (p i).reverse = reflect N (∑ i ∈ s, p i)

Reflection of a sum at a fixed length = sum of reverses, when all degrees agree. If every p i (i ∈ s) has natDegree = N, then Σ reverse (p i) = reflect N (Σ p i). Each reverse (p i) = reflect (natDegree (p i)) (p i) = reflect N (p i), and reflect N is additive (reflect_add), so it commutes with the finite sum. This packages the degree-bookkeeping that lets the per-vertex/per-root reversed pieces of the moment theorem be summed under a single reflection.

theorem Polynomial.sum_map_reverse_eq_reflect_sum {R : Type u_1} [CommRing R] (m : Multiset (Polynomial R)) (N : ℕ) (hp : ∀ p ∈ m, p.natDegree = N) : (Multiset.map reverse m).sum = reflect N m.sum

Multiset form of sum_reverse_eq_reflect_sum: if every polynomial in m has natDegree = N, then (m.map reverse).sum = reflect N m.sum. Same proof (reflect_add additivity, reverse = reflect natDegree), over a multiset rather than a Finset.

theorem Polynomial.reflect_X_mul_derivative_eq_sum_prod (p : Polynomial ℂ) (hm : p.Monic) : (Multiset.map (fun (a : ℂ) => (Multiset.map (fun (b : ℂ) => 1 - C b * X) (p.roots.erase a)).prod) p.roots).sum = reflect p.natDegree (X * derivative p)

(PB) Matching-side polynomial identity. For a monic split p over ℂ, the sum over its roots of the "leave-one-out" reversed-factor products equals the reflected X·p':

Σ_{θ∈roots} ∏_{φ∈roots.erase θ}(1 - φX) = reflect_n(X · p'), n = natDegree p.

This is the polynomial heart of the matching side of the moment theorem. p splits as ∏(X-θ) (Splits.eq_prod_roots_of_monic), so p' = Σ_θ ∏_{erase}(X-φ) (derivative_prod_X_sub_C, B2), and X·p' = Σ_θ X·∏_{erase}; each X·∏_{erase} has natDegree = n (natDegree_X_mul + the product-of-(n-1)-monic-linears degree), so the reflected sum splits termwise (sum_map_reverse_eq_reflect_sum) into Σ_θ reverse(X·∏_{erase}) = Σ_θ ∏_{erase}(1-φX) via reverse_X_mul + reverse_prod_X_sub_C.

theorem Polynomial.mk_powerSum_mul_reverse (p : Polynomial ℂ) (hm : p.Monic) : (PowerSeries.mk fun (k : ℕ) => (Multiset.map (fun (x : ℂ) => x ^ k) p.roots).sum) * ↑p.reverse = ↑(reflect p.natDegree (X * derivative p))

(M5-core) Matching generating function times the reversed polynomial. For a monic p over ℂ, the generating function of the power sums of its roots, times ↑reverse p, is ↑reflect_n(X·p'):

mk (Σ_θ θᵏ) · ↑reverse p = ↑reflect_n(X · p'), n = natDegree p.

mk (Σ_θ θᵏ) = Σ_θ geomSeries θ (powerSum_genfun); ↑reverse p = ∏_θ (1 - θX) in ℂ⟦X⟧ (splitting + reverse_prod_X_sub_C + the coercion of a polynomial product); so by geomSeries_sum_mul_prod () the product collapses to Σ_θ ∏_{erase}(1 - φX), which is ↑ of the polynomial identity reflect_X_mul_derivative_eq_sum_prod (PB).

theorem SimpleGraph.adjMatrix_deleteIncidenceSet_self {V : Type u_1} [DecidableEq V] {R : Type u_2} [CommRing R] (G : SimpleGraph V) [DecidableRel G.Adj] (r : V) : adjMatrix R (G.deleteIncidenceSet r) r = 0

The r-th row of the adjacency matrix of G.deleteIncidenceSet r is zero: deleting all edges incident to r makes r isolated, so r is adjacent to nothing.

theorem SimpleGraph.adjMatrix_submatrix_deleteIncidenceSet {V : Type u_1} [DecidableEq V] {R : Type u_2} [CommRing R] (G : SimpleGraph V) [DecidableRel G.Adj] (r : V) : (adjMatrix R (G.deleteIncidenceSet r)).submatrix Subtype.val Subtype.val = (adjMatrix R G).submatrix Subtype.val Subtype.val

The {≠r} principal submatrix is unaffected by deleting the edges at r: an entry between two vertices ≠ r is an edge of G.deleteIncidenceSet r iff it is an edge of G.

theorem SimpleGraph.coe_charpolyRev_adjMatrix_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] {R : Type u_2} [CommRing R] (G : SimpleGraph V) [DecidableRel G.Adj] (r : V) : ↑(adjMatrix R (G.deleteIncidenceSet r)).charpolyRev = ↑((adjMatrix R G).submatrix Subtype.val Subtype.val).charpolyRev

(M1) charpolyRev reconciliation: deleting all edges at the root = deleting the root index. ↑charpolyRev(A(G.deleteIncidenceSet r)) = ↑charpolyRev(A(G)∖r) in R⟦X⟧. A(G.deleteIncidenceSet r) has a zero row at r, so 1 - X·A(deleteIncidenceSet r) has row r equal to eᵣ; its determinant collapses to the {≠r} minor (det_eq_det_submatrix_ne_of_row_eq_single), whose blocks agree with A(G)∖r (adjMatrix_submatrix_deleteIncidenceSet). This bridges the submatrix form of Lemma 3 (resolventSeries_diag_mul_coe_charpolyRev) to the isolated-root path tree of godsil_resolvent_charpoly_form.

theorem SimpleGraph.resolventSeries_pathTree_mul_reverse_matchingPoly {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : (adjMatrix ℝ (G.pathTree v)).resolventSeries (G.pathTreeRoot v) (G.pathTreeRoot v) * ↑G.matchingPoly.reverse = ↑(G.deleteIncidenceSet v).matchingPoly.reverse

(M3) Per-vertex resolvent identity. The root–root resolvent of the path tree T_v, times the reversed matching polynomial of G, equals the reversed matching polynomial of G with all edges at v deleted:

(Σ_k [A(T_v)ᵏ]_{rr} Xᵏ) · ↑reverse μ(G) = ↑reverse μ(G.deleteIncidenceSet v).

Assembled from Lemma 3 (resolventSeries_diag_mul_coe_charpolyRev, submatrix form) reconciled to the isolated-root tree (M1, coe_charpolyRev_adjMatrix_deleteIncidenceSet), the reversed Godsil identity (godsil_resolvent_charpoly_form under reverse_mul_of_domain over the domain ℝ[X], with reverse_charpoly swapping reverse ∘ charpoly = charpolyRev), and cancellation of the unit factor ↑charpolyRev(A T_v) (nonzero: charpoly is monic, reverse preserves nonzero). This is the trace side reduced to the same reversed matching polynomials the matching side speaks.

theorem SimpleGraph.adjMatrix_pow_apply_cast {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (k : ℕ) (i j : V) : ↑((adjMatrix ℕ H ^ k) i j) = (adjMatrix ℝ H ^ k) i j

The ℕ-valued and ℝ-valued adjacency-matrix powers agree under the cast ℕ → ℝ: the adjacency matrix over ℝ is the entrywise cast of the one over ℕ (adjMatrix_apply + apply_ite), and casting commutes with matrix powers (Matrix.map_pow).

theorem SimpleGraph.mk_treeLikeWalkCount_eq_sum_resolventSeries {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (PowerSeries.mk fun (k : ℕ) => ↑(treeLikeWalkCount k)) = ∑ v : V, (adjMatrix ℝ (G.pathTree v)).resolventSeries (G.pathTreeRoot v) (G.pathTreeRoot v)

(M4a) Trace generating function as a sum of path-tree resolvents. The generating function of the tree-like-walk counts is the sum over vertices of the root–root resolvent of each path tree: mk (tlwc G ·) = Σ_v resolventSeries(A T_v)_{rr} (over ℝ). Lemma 1 (treeLikeWalkCount_eq_sum_pathTree_adjMatrix_pow) coefficientwise, with the ℕ→ℝ cast.

theorem SimpleGraph.mk_treeLikeWalkCount_mul_reverse_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (PowerSeries.mk fun (k : ℕ) => ↑(treeLikeWalkCount k)) * ↑G.matchingPoly.reverse = ↑(Polynomial.reflect (Fintype.card V) (Polynomial.X * Polynomial.derivative G.matchingPoly))

(M4) Trace side reduced to the reflected derivative. The tree-like-walk generating function, times ↑reverse μ(G), equals ↑reflect_n(X·μ'(G)) (n = card V):

mk (tlwc G ·) · ↑reverse μ(G) = ↑reflect_n(X · μ'(G)).

Sum the per-vertex resolvent identity (M3) over v (Finset.sum_mul), push the coercion through the sum, collapse Σ_v reverse μ(G.deleteIncidenceSet v) = reflect_n(Σ_v μ(G.deleteIncidenceSet v)) (sum_reverse_eq_reflect_sum, every μ(G−v) has natDegree = n), and apply the vertex-deletion law Σ_v μ(G.deleteIncidenceSet v) = X·μ'. The whole trace side now lives in the reflected matching polynomials — the exact object the matching side produces.

theorem SimpleGraph.mk_matchingPowerSum_mul_reverse_eq {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (PowerSeries.mk fun (k : ℕ) => matchingPowerSum k) * ↑(Polynomial.map (algebraMap ℝ ℂ) G.matchingPoly).reverse = ↑(Polynomial.reflect (Fintype.card V) (Polynomial.X * Polynomial.derivative (Polynomial.map (algebraMap ℝ ℂ) G.matchingPoly)))

(M5) Matching side reduced to the reflected derivative. Specialise mk_powerSum_mul_reverse to μ_ℂ = μ(G).map(ℝ→ℂ) (monic, natDegree = card V):

mk (matchingPowerSum G ·) · ↑reverse μ_ℂ = ↑reflect_n(X · μ_ℂ'), n = card V.

The matching generating function now lives in the same reflected matching polynomials as the trace side (M4), the two halves ready to be welded after the ℝ→ℂ bridge.

theorem SimpleGraph.matchingPowerSum_eq_treeLikeWalkCount {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : matchingPowerSum k = ↑(treeLikeWalkCount k)

Godsil's moment theorem. matchingPowerSum G k = treeLikeWalkCount G k: the k-th power sum of the roots of the matching polynomial equals the number of closed tree-like walks of length k.

The trace side (M4, over ℝ) and the matching side (M5, over ℂ) both equal ↑reflect_n(X·μ'). Mapping M4 along ℝ → ℂ (the coercion commutes with map, reverse, reflect, derivative) gives mk(tlwc) · ↑reverse μ_ℂ = ↑reflect_n(X·μ_ℂ'), matching M5. Since ↑reverse μ_ℂ is a unit (μ_ℂ monic ⇒ nonzero), the two generating functions coincide; the k-th coefficient is the theorem.