Real-rootedness of the matching polynomial

For a forest, the only permutations that contribute to the determinant expansion of the characteristic polynomial of the adjacency matrix are the involutions whose 2-cycles are edges, so the matching polynomial of a forest is the characteristic polynomial of its adjacency matrix, which is real-rooted because the matrix is symmetric. Path-tree divisibility then transfers real-rootedness to connected graphs, and the product over components to all finite graphs: this is the real-rootedness part of the Heilmann–Lieb theorem.

Main results

• SimpleGraph.charpoly_symmetric_realRooted: the characteristic polynomial of a real symmetric matrix is real-rooted.
• SimpleGraph.matchingPoly_forest_eq_charpoly: μ(F) = charpoly (adjMatrix F) for a forest F.
• SimpleGraph.matchingPoly_forest_realRooted, SimpleGraph.matchingPoly_connected_realRooted.
• SimpleGraph.matchingPoly_realRooted: the matching polynomial of every finite graph is real-rooted.

References

• O. J. Heilmann, E. H. Lieb, Theory of monomer-dimer systems, Comm. Math. Phys. 25 (1972) 190–232.
• C. D. Godsil, Matchings and walks in graphs, J. Graph Theory 5 (1981) 285–297.

theorem MSS.charpoly_symmetric_realRooted {V : Type u_1} [Fintype V] [DecidableEq V] {A : Matrix V V ℝ} (hA : A.IsSymm) : RealRooted A.charpoly

charpoly of a real symmetric matrix is real-rooted. Over ℝ a symmetric matrix is Hermitian (star is trivial, so Aᴴ = Aᵀ = A), and this is Mathlib's Matrix.IsHermitian.splits_charpoly.

theorem SimpleGraph.signingMatrix_const_true {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] : (G.signingMatrix fun (x : Sym2 V) => true) = adjMatrix ℝ G

The all-+ signing matrix is exactly the (unsigned) adjacency matrix over ℝ: every edge gets the entry +1, off the edge set 0.

theorem SimpleGraph.acyclic_perm_support_isInvolution {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (hac : G.IsAcyclic) {σ : Equiv.Perm V} (hsupp : ∀ (i : V), σ i ≠ i → G.Adj (σ i) i) : σ ^ 2 = 1

The forest involution lemma. On a forest (IsAcyclic), any permutation σ whose every non-fixed point is adjacent to its image is an involution σ² = 1. If not, some x has a σ-orbit of minimal period p ≥ 3; its consecutive points x, σx, …, σ^{p-1}x are distinct and adjacent, so deleting the edge {x, σx} still leaves x and σx connected (go around the orbit the long way, σx → σ²x → ⋯ → σ^p x = x), i.e. {x, σx} is not a bridge — contradicting isAcyclic_iff_forall_edge_isBridge. This is the combinatorial heart of "matching polynomial = characteristic polynomial on a forest": in the permutation expansion of charpoly(A) the surviving terms are exactly the matchings.

theorem SimpleGraph.matchingPoly_forest_realRooted_of_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (heq : G.matchingPoly = (adjMatrix ℝ G).charpoly) : MSS.RealRooted G.matchingPoly

A forest's matching polynomial is real-rooted. Immediate from μ(F) = charpoly(A) and charpoly of the symmetric adjacency matrix being real-rooted.

μ(forest) = charpoly via the permutation expansion

theorem SimpleGraph.prod_support_const_true_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {σ : Equiv.Perm V} (hP : G.IsEdgeInvolution σ) : ∏ i ∈ σ.support, -Polynomial.C (G.signingMatrix (fun (x : Sym2 V) => true) (σ i) i) = 1

On the all-+ signing (= adjacency matrix), each support factor is −C 1 = −1, so an edge-involution's support product is (−1)^{|support|} = (−1)^{2|M|} = 1.

theorem SimpleGraph.prod_support_const_true_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hac : G.IsAcyclic) {σ : Equiv.Perm V} (hP : ¬G.IsEdgeInvolution σ) : ∏ i ∈ σ.support, -Polynomial.C (G.signingMatrix (fun (x : Sym2 V) => true) (σ i) i) = 0

On a forest, a permutation that is not an edge-involution must have a non-adjacent support pair (if all its support pairs were edges it would be an involution, by acyclic_perm_support_isInvolution), so its support product vanishes.

theorem SimpleGraph.matchingPoly_forest_eq_charpoly {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hac : G.IsAcyclic) : G.matchingPoly = (adjMatrix ℝ G).charpoly

For a forest, the matching polynomial equals the characteristic polynomial of the adjacency matrix: μ(F) = charpoly(A). The permutation expansion of charpoly(A) restricts to edge-involutions — non-edge-involutions vanish (a non-adjacent support pair, or, on a forest, the involution lemma forces one) — and edge-involutions biject with matchings carrying the sign (−1)^{|M|}, reassembling μ(G).

theorem SimpleGraph.matchingPoly_forest_realRooted {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hac : G.IsAcyclic) : MSS.RealRooted G.matchingPoly

A forest's matching polynomial is real-rooted.

theorem SimpleGraph.matchingPoly_connected_realRooted {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) : MSS.RealRooted G.matchingPoly

Connected real-rootedness. The matching polynomial of any connected finite graph is real-rooted. Godsil's path-tree divisibility gives μ(G) ∣ μ(T(G,u)) for a vertex u (which exists since G is connected hence nonempty); the path tree is a forest (pathTree_isAcyclic), so μ(T(G,u)) is real-rooted; and a nonzero divisor of a real-rooted polynomial is real-rooted (RealRooted.of_dvd). The path tree is monic, hence nonzero.

theorem SimpleGraph.matchingPoly_realRooted {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : MSS.RealRooted G.matchingPoly

Heilmann–Lieb real-rootedness. The matching polynomial of any finite graph is real-rooted. μ(G) = ∏_C μ(G[C.supp]) over connected components (matchingPoly_eq_prod_components); each induced component is connected (ConnectedComponent.maximal_connected_induce_supp), so its matching polynomial is real-rooted; and real-rootedness is closed under finite products (RealRooted.prod).