The vertex-deletion derivative law for the matching polynomial

Summing over the vertices v the number of k-matchings avoiding v counts each k-matching once for each of its n - 2k uncovered vertices. Consequently ∑_v μ(G - v) = X · μ'(G), where G - v keeps v as an isolated vertex.

Main results

• SimpleGraph.sum_matchingNumber_deleteIncidenceSet: ∑_v m_k(G - v) = (n - 2k) m_k(G).
• SimpleGraph.sum_matchingPoly_deleteIncidenceSet: ∑_v μ(G - v) = X · μ'(G).

References

• C. D. Godsil, Algebraic Combinatorics, Chapman & Hall, 1993, Chapter 1.

theorem SimpleGraph.card_uncovered_of_mem_matchingsOfCard {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {k : ℕ} {s : Finset (Sym2 V)} (hs : s ∈ G.matchingsOfCard k) : {w : V | ∀ e ∈ s, w ∉ e}.card = Fintype.card V - 2 * k

A k-matching covers exactly 2k vertices, hence leaves n − 2k uncovered: #{ v : ∀ e ∈ s, v ∉ e } = n − 2k.

theorem SimpleGraph.sum_matchingNumber_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : ∑ v : V, (G.deleteIncidenceSet v).matchingNumber k = (Fintype.card V - 2 * k) * G.matchingNumber k

The vertex-deletion double-count Σ_v m_k(G−v) = (n − 2k)·m_k(G): summing, over all vertices v, the k-matchings of G−v (= the k-matchings of G avoiding v) tallies each k-matching once for each of its n − 2k uncovered vertices. This is the combinatorial heart of Godsil's moment theorem.

theorem SimpleGraph.X_mul_derivative_X_pow (m : ℕ) : Polynomial.X * Polynomial.derivative (Polynomial.X ^ m) = Polynomial.C ↑m * Polynomial.X ^ m

X · d/dX (Xᵐ) = C(m) · Xᵐ — handles the m = 0 boundary cleanly (both sides 0).

theorem SimpleGraph.sum_matchingPoly_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∑ v : V, (G.deleteIncidenceSet v).matchingPoly = Polynomial.X * Polynomial.derivative G.matchingPoly

The vertex-deletion derivative law Σ_v μ(G−v) = X·μ'(G) (fixed-n incidence-deletion form: G.deleteIncidenceSet v isolates v, so μ(G.deleteIncidenceSet v) plays the role of X·μ(G−v)). The matching-polynomial mirror of char'(A) = Σ_v char(A_v̂), and the log-derivative μ'/μ = Σ_v μ(G−v)/μ(G) opening Godsil's tree-like-walk generating function. Termwise from the double-count sum_matchingNumber_deleteIncidenceSet.