The matching polynomial of a finite graph

For a finite simple graph G on n vertices with m_k matchings of k edges, the matching polynomial is μ(G) = ∑_k (-1)^k m_k X^(n - 2k). This file defines it together with the monomer-dimer partition function P(G) = ∑_k m_k X^k, and proves the vertex-deletion recurrence.

Main definitions

• SimpleGraph.IsMatchingSet s: the edges in s are pairwise disjoint.
• SimpleGraph.matchingNumber G k: the number m_k of k-edge matchings.
• SimpleGraph.matchingPoly G: the matching polynomial, over ℝ.
• SimpleGraph.matchingPartition G: the partition function ∑_k m_k X^k.

Main results

• SimpleGraph.matchingPoly_monic, SimpleGraph.matchingPoly_degree: μ(G) is monic of degree n.
• SimpleGraph.matchingPoly_iso: μ is invariant under graph isomorphism.
• SimpleGraph.matchingNumber_recurrence: m_{k+1}(G) = m_{k+1}(G - v) + ∑_{u ∼ v} m_k(G - v - u), with vertex deletion realized as deleteIncidenceSet (the vertex stays, isolated).
• SimpleGraph.matchingPartition_recurrence: P(G) = P(G - v) + X ∑_{u ∼ v} P(G - v - u).
• SimpleGraph.matchingPoly_recurrence: X² μ(G) = X² μ(G - v) - ∑_{u ∼ v} μ(G - v - u) with isolated-vertex deletion.
• SimpleGraph.dvd_of_godsil_identity: the algebraic step from Godsil's identity to divisibility.

References

• C. D. Godsil, I. Gutman, On the theory of the matching polynomial, J. Graph Theory 5 (1981) 137–144.
• C. D. Godsil, Algebraic Combinatorics, Chapman & Hall, 1993, Chapter 1.

def SimpleGraph.IsMatchingSet {V : Type u_1} (s : Finset (Sym2 V)) : Prop

A finset of edges is a matching set if its edges are pairwise vertex-disjoint (no vertex lies in two of them).

Equations

• SimpleGraph.IsMatchingSet s = ∀ e ∈ s, ∀ f ∈ s, e ≠ f → ∀ v ∈ e, v ∉ f

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

The finset of k-edge matchings of G: k-subsets of the edge set whose edges are pairwise disjoint.

Equations

• G.matchingsOfCard k = Finset.filter SimpleGraph.IsMatchingSet (Finset.powersetCard k G.edgeFinset)

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

The matching number m_k = #{k-edge matchings} of G.

Equations

• G.matchingNumber k = (G.matchingsOfCard k).card

noncomputable def SimpleGraph.matchingPoly {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Polynomial ℝ

The matching polynomial μ(G, x) = Σ_k (-1)^k m_k x^{n-2k}, summed over k ≤ n/2 (a matching of k edges covers 2k ≤ n vertices).

Equations

• G.matchingPoly = ∑ k ∈ Finset.range (Fintype.card V / 2 + 1), Polynomial.C ((-1) ^ k * ↑(G.matchingNumber k)) * Polynomial.X ^ (Fintype.card V - 2 * k)

theorem SimpleGraph.matchingNumber_zero {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingNumber 0 = 1

The empty matching. There is exactly one 0-edge matching (the empty set), so m_0 = 1. This is the leading coefficient of μ(G) and the base anchor that the definition behaves.

Heilmann–Lieb by interlacing — first step: the base case

theorem SimpleGraph.matchingNumber_bot {V : Type u_1} [Fintype V] (k : ℕ) : ⊥.matchingNumber k = if k = 0 then 1 else 0

For the edgeless graph ⊥, the only matching is the empty one: m_k = 1 if k = 0, else 0.

theorem SimpleGraph.matchingPoly_bot {V : Type u_1} [Fintype V] : ⊥.matchingPoly = Polynomial.X ^ Fintype.card V

Base case of the Heilmann–Lieb induction. The matching polynomial of the edgeless graph is μ(⊥) = X^n (all roots 0, trivially in the band).

theorem SimpleGraph.matchingPoly_bot_realRooted {V : Type u_1} [Fintype V] : MSS.RealRooted ⊥.matchingPoly

The base case is real-rooted: μ(⊥) = X^n splits over ℝ (root 0, multiplicity n). The anchor of the interlacing induction toward Heilmann–Lieb.

Degree and monicity of μ(G)

theorem SimpleGraph.matchingPoly_eq_X_pow_add_erase {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingPoly = Polynomial.X ^ Fintype.card V + ∑ k ∈ (Finset.range (Fintype.card V / 2 + 1)).erase 0, Polynomial.C ((-1) ^ k * ↑(G.matchingNumber k)) * Polynomial.X ^ (Fintype.card V - 2 * k)

μ(G) with its leading (k = 0) term X^n split off. The k=0 summand is C((-1)^0 · m_0) X^{n-0} = X^n (since m_0 = 1); the rest are the lower terms.

theorem SimpleGraph.matchingPoly_erase_degree_lt {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (∑ k ∈ (Finset.range (Fintype.card V / 2 + 1)).erase 0, Polynomial.C ((-1) ^ k * ↑(G.matchingNumber k)) * Polynomial.X ^ (Fintype.card V - 2 * k)).degree < ↑(Fintype.card V)

The non-leading terms of μ(G) all have degree < n = |V|: term k ≥ 1 has degree ≤ n - 2k < n.

theorem SimpleGraph.matchingPoly_monic {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingPoly.Monic

μ(G) is monic. Its leading term is the k=0 summand X^n.

theorem SimpleGraph.matchingPoly_degree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingPoly.degree = ↑(Fintype.card V)

deg μ(G) = n = |V|.

@[simp]

theorem SimpleGraph.matchingPoly_natDegree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.matchingPoly.natDegree = Fintype.card V

Vertex deletion (first step of the matching recurrence)

theorem SimpleGraph.mem_edgeSet_deleteIncidenceSet {V : Type u_1} (G : SimpleGraph V) (v : V) (e : Sym2 V) : e ∈ (G.deleteIncidenceSet v).edgeSet ↔ e ∈ G.edgeSet ∧ v ∉ e

Vertex deletion, edge level. G.deleteIncidenceSet v (Mathlib) is G with all edges at v removed — v becomes isolated, the vertex type V is preserved (no subtypes). An edge survives iff it was an edge of G not containing v. This is the foundational identity of the matching recurrence: a matching of G that avoids v is exactly a matching of G.deleteIncidenceSet v.

theorem SimpleGraph.notMem_of_mem_edgeSet_deleteIncidenceSet {V : Type u_1} (G : SimpleGraph V) (v : V) {e : Sym2 V} (he : e ∈ (G.deleteIncidenceSet v).edgeSet) : v ∉ e

v is isolated after deletion. No surviving edge contains v. The clean statement of "vertex v removed": every matching of G.deleteIncidenceSet v avoids v, which is what the v-not-covered branch of the recurrence needs.

theorem SimpleGraph.edgeSet_deleteIncidenceSet_subset {V : Type u_1} (G : SimpleGraph V) (v : V) : (G.deleteIncidenceSet v).edgeSet ⊆ G.edgeSet

The deleted graph is a subgraph: every edge of G.deleteIncidenceSet v is an edge of G.

Count decomposition, branch (a): matchings avoiding v

theorem SimpleGraph.mem_edgeFinset_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (e : Sym2 V) : e ∈ (G.deleteIncidenceSet v).edgeFinset ↔ e ∈ G.edgeFinset ∧ v ∉ e

The edgeFinset version of mem_edgeSet_deleteIncidenceSet.

theorem SimpleGraph.matchingsOfCard_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (k : ℕ) : (G.deleteIncidenceSet v).matchingsOfCard k = {s ∈ G.matchingsOfCard k | ∀ e ∈ s, v ∉ e}

Decomposition, the v-avoiding branch. The k-matchings of G.deleteIncidenceSet v are exactly the k-matchings of G that avoid v:

  (G−v).matchingsOfCard k = (G.matchingsOfCard k).filter (no edge contains v).

This is the first half of the matching recurrence m_k(G) = m_k(G−v) + …: the matchings not covering v are precisely those of the deleted graph.

theorem SimpleGraph.matchingNumber_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (k : ℕ) : (G.deleteIncidenceSet v).matchingNumber k = {s ∈ G.matchingsOfCard k | ∀ e ∈ s, v ∉ e}.card

Consequently the matching number of G−v counts the v-avoiding k-matchings of G.

Count decomposition, branch (b): matchings covering v

theorem SimpleGraph.mem_edgeSet_deleteIncidenceSet_two {V : Type u_1} (G : SimpleGraph V) (v u : V) (e : Sym2 V) : e ∈ ((G.deleteIncidenceSet v).deleteIncidenceSet u).edgeSet ↔ e ∈ G.edgeSet ∧ v ∉ e ∧ u ∉ e

Double deletion, edge level. G − v − u (delete the incidence sets of both v and u) keeps exactly the edges of G containing neither.

theorem SimpleGraph.matchingsOfCard_deleteIncidenceSet_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v u : V) (k : ℕ) : ((G.deleteIncidenceSet v).deleteIncidenceSet u).matchingsOfCard k = {s ∈ G.matchingsOfCard k | (∀ e ∈ s, v ∉ e) ∧ ∀ e ∈ s, u ∉ e}

G − v − u matchings = G matchings avoiding both v and u. Composing the v-avoiding branch twice. This is the codomain side of branch (b): removing the edge {v,u} from a k-matching of G covering v (via u) lands in the (k−1)-matchings of G − v − u.

theorem SimpleGraph.IsMatchingSet.subset {V : Type u_1} {s t : Finset (Sym2 V)} (hs : IsMatchingSet s) (hts : t ⊆ s) : IsMatchingSet t

Matchings are subset-closed. Removing edges from a matching keeps a matching — the erase-the-{v,u}-edge direction of the branch-(b) bijection.

theorem SimpleGraph.IsMatchingSet.insert {V : Type u_1} [DecidableEq V] {e : Sym2 V} {t : Finset (Sym2 V)} (ht : IsMatchingSet t) (hd : ∀ f ∈ t, ∀ w ∈ e, w ∉ f) (hd' : ∀ f ∈ t, ∀ w ∈ f, w ∉ e) : IsMatchingSet (Insert.insert e t)

Inserting a disjoint edge keeps a matching. If e shares no vertex with any edge of the matching t, then insert e t is a matching — the insert-the -{v,u}-edge direction of the branch-(b) bijection.

theorem SimpleGraph.mem_edgeFinset_deleteIncidenceSet_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v u : V) (e : Sym2 V) : e ∈ ((G.deleteIncidenceSet v).deleteIncidenceSet u).edgeFinset ↔ e ∈ G.edgeFinset ∧ v ∉ e ∧ u ∉ e

The edgeFinset version of mem_edgeSet_deleteIncidenceSet_two.

theorem SimpleGraph.mem_matchingsOfCard {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} {s : Finset (Sym2 V)} : s ∈ G.matchingsOfCard k ↔ s ⊆ G.edgeFinset ∧ s.card = k ∧ IsMatchingSet s

Membership in matchingsOfCard: a k-edge subset of the edge set that is a matching.

Isomorphism invariance of μ

theorem SimpleGraph.image_map_mem_matchingsOfCard {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {W : Type u_2} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (e : G ≃g H) {k : ℕ} {s : Finset (Sym2 V)} (hs : s ∈ G.matchingsOfCard k) : Finset.image (Sym2.map ⇑e) s ∈ H.matchingsOfCard k

A graph isomorphism carries k-matchings to k-matchings (image under Sym2.map e): edges go to edges (map_mem_edgeSet_iff), the matching condition is preserved (e injective on vertices), and the cardinality is unchanged (Sym2.map e injective).

theorem SimpleGraph.matchingNumber_iso {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {W : Type u_2} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (e : G ≃g H) (k : ℕ) : G.matchingNumber k = H.matchingNumber k

The matching numbers are isomorphism invariants.

theorem SimpleGraph.matchingPoly_iso {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {W : Type u_2} [Fintype W] [DecidableEq W] {H : SimpleGraph W} [DecidableRel H.Adj] (e : G ≃g H) : G.matchingPoly = H.matchingPoly

μ is an isomorphism invariant. This lets the matching polynomial of each subtree T(G−u, b) be read off through the structural iso prependRoot_grows, en route to the root-decomposition product μ(T−r) = X·∏_{b∼u} μ(T(G−u,b)).

theorem SimpleGraph.matchingPoly_inst_irrel {V : Type u_2} (fV₁ fV₂ : Fintype V) (G : SimpleGraph V) (rG₁ rG₂ : DecidableRel G.Adj) : G.matchingPoly = G.matchingPoly

μ is independent of the Fintype/Decidable instances. All three are Subsingletons, so μ(G) computed with any pair of instance choices agree. This lets a matchingPoly term produced by one elaboration path (e.g. an iso transport) be matched against one produced by another (e.g. a direct Σ-decomposition) propositionally, without forcing isDefEq to whnf-reduce the polynomial — which over a Σ-type blows the heartbeat budget.

theorem SimpleGraph.card_filter_covering {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {v u : V} (huv : G.Adj v u) (k : ℕ) : {w ∈ G.matchingsOfCard (k + 1) | s(v, u) ∈ w}.card = ((G.deleteIncidenceSet v).deleteIncidenceSet u).matchingNumber k

The branch-(b) bijection. For a neighbour u ∼ v, the (k+1)-matchings of G that cover v via the edge {v,u} are in bijection (erase / insert that edge) with the k-matchings of G − v − u:

  #{w ∈ matchingsOfCard (k+1) | s(v,u) ∈ w} = m_k(G − v − u).

This is the v-covering half of the matching recurrence..

theorem SimpleGraph.matchingNumber_recurrence {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (k : ℕ) : G.matchingNumber (k + 1) = (G.deleteIncidenceSet v).matchingNumber (k + 1) + ∑ u ∈ G.neighborFinset v, ((G.deleteIncidenceSet v).deleteIncidenceSet u).matchingNumber k

The matching-number recurrence. Deleting a vertex v:

  m_{k+1}(G) = m_{k+1}(G − v) + ∑_{u ∼ v} m_k(G − v − u).

A (k+1)-matching of G either avoids v (a (k+1)-matching of G − v, branch (a)) or covers v via a unique edge {v,u} with u ∼ v (bijecting with a k-matching of G − v − u, branch (b)). The covering matchings partition over the neighbour u matched to v (unique, since a matching has one edge at v).

def SimpleGraph.matchingPoly_recurrence_target {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : Prop

Polynomial recurrence (target — statement type-checks). The count recurrence lifts to the matching polynomial. Because deleteIncidenceSet keeps the deleted vertex isolated (fixed vertex count n), each deletion pads μ by a factor X, so the recurrence carries an X²:

  X² · μ(G) = X² · μ(G−v) − ∑_{u∼v} μ(G−v−u).

Verified numerically on the edge and P₃. Mathematically clean (index shift j = k−1, the X² absorbing the X^{-2} from the shift); the Lean proof is a Finset.sum reindexing over the ℕ-exponents n − 2k of the definition. Equivalent (divide by X²) to the textbook μ(G) = X·μ'(G−v) − Σ μ''(G−v−u) with true (n−1)/(n−2)-vertex deletions. Proved as matchingPoly_recurrence.

Equations

• One or more equations did not get rendered due to their size.

The clean recurrence via the monomer-dimer partition function

theorem SimpleGraph.matchingNumber_eq_zero_of_card_lt {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {k : ℕ} (h : Fintype.card V < 2 * k) : G.matchingNumber k = 0

Matching-size bound (the one gap). A k-matching covers 2k distinct vertices, so if n < 2k there is none: m_k(G) = 0. Each edge of a matching contributes 2 distinct vertices (Sym2.card_toFinset_of_not_isDiag), pairwise disjoint (the matching condition), so card_biUnion gives 2k covered vertices, ≤ n.

noncomputable def SimpleGraph.matchingPartition {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Polynomial ℝ

The monomer-dimer partition function P(G, X) = ∑_k m_k(G) X^k (dimers weighted by X, monomers by 1). Unlike matchingPoly, this carries no signs and no fixed-n exponent shift, so its deletion recurrence is clean.

Equations

• G.matchingPartition = ∑ k ∈ Finset.range (Fintype.card V + 1), Polynomial.C ↑(G.matchingNumber k) * Polynomial.X ^ k

theorem SimpleGraph.matchingPartition_coeff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : G.matchingPartition.coeff d = ↑(G.matchingNumber d)

The coefficients of P(G, X) are exactly the matching numbers (the bound kills everything past the range).

The bridge μ ↔ P: reflect_card μ(G) = P(G) ∘ (−X²)

The matching polynomial μ(G,x) = Σ (-1)^k m_k x^{n-2k} and the partition function P(G,X) = Σ m_k X^k are reverses of each other after the substitution X ↦ -X²: reflecting μ(G) at degree n sends X^{n-2k} ↦ X^{2k}, exactly P(G) evaluated at -X² (the sign (-1)^k coming from (-X²)^k). This is the load-bearing identity that transfers the real-rootedness / root-bound of P (where the interlacing machinery lives) to μ (where Heilmann–Lieb states the Ramanujan band), and it makes μ multiplicative on disjoint unions out of the clean P-multiplicativity.

theorem SimpleGraph.matchingPoly_reflect_card {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Polynomial.reflect (Fintype.card V) G.matchingPoly = G.matchingPartition.comp (Polynomial.C (-1) * Polynomial.X ^ 2)

theorem SimpleGraph.matchingPartition_recurrence {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : G.matchingPartition = (G.deleteIncidenceSet v).matchingPartition + Polynomial.X * ∑ u ∈ G.neighborFinset v, ((G.deleteIncidenceSet v).deleteIncidenceSet u).matchingPartition

The clean recurrence. Deleting a vertex v:

  P(G) = P(G − v) + X · ∑_{u ∼ v} P(G − v − u).

No signs, no X²: the partition function lifts the count recurrence directly. Proved coefficient-wise via matchingNumber_recurrence..

The signed vertex-deletion recurrence for μ (lifts the clean P recurrence)

theorem SimpleGraph.reflect_finsetSum {ι : Type u_2} (N : ℕ) (s : Finset ι) (f : ι → Polynomial ℝ) : Polynomial.reflect N (∑ i ∈ s, f i) = ∑ i ∈ s, Polynomial.reflect N (f i)

reflect distributes over a finite sum.

theorem SimpleGraph.comp_finsetSum {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial ℝ) (r : Polynomial ℝ) : (∑ i ∈ s, f i).comp r = ∑ i ∈ s, (f i).comp r

comp distributes over a finite sum (in the composed polynomial).

theorem SimpleGraph.reflect_card_add_two_Xsq_mul {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Polynomial.reflect (Fintype.card V + 2) (Polynomial.X ^ 2 * G.matchingPoly) = Polynomial.reflect (Fintype.card V) G.matchingPoly

Reflecting X²·μ(G) at degree n+2 lands on reflect_n μ(G) (both = P(G)∘(−X²)): the extra X² is exactly absorbed by the two-larger reflection degree.

theorem SimpleGraph.reflect_card_add_two {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Polynomial.reflect (Fintype.card V + 2) G.matchingPoly = Polynomial.X ^ 2 * Polynomial.reflect (Fintype.card V) G.matchingPoly

Reflecting μ(G) at degree n+2 introduces one factor X² over reflect_n μ(G).

theorem SimpleGraph.matchingPoly_recurrence {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : G.matchingPoly_recurrence_target v

The signed vertex-deletion recurrence X²·μ(G) = X²·μ(G−v) − Σ_{u∼v} μ(G−v−u) (matchingPoly_recurrence_target). Proved by reflecting at degree n+2 (an injection, via reflect_reflect) and using the μ ↔ P bridge to reduce to the already-proved clean partition recurrence matchingPartition_recurrence, pushed through comp (−X²). This is the engine of Godsil's identity μ(G)·μ(T−r) = μ(G−a)·μ(T), hence of the path-tree divisibility μ(G) ∣ μ(T(G,u)).

theorem SimpleGraph.dvd_of_godsil_identity {μG μGa μT μTr : Polynomial ℝ} (hGa : μGa ≠ 0) (hid : μG * μTr = μGa * μT) (hdvd : μGa ∣ μTr) : μG ∣ μT

Divisibility transfer — the algebraic core of Godsil's path-tree induction. Given Godsil's identity μ(G)·μ(T−r) = μ(G−a)·μ(T) (hid) and the inductive divisibility μ(G−a) ∣ μ(T−r) (hdvd), with μ(G−a) ≠ 0, conclude μ(G) ∣ μ(T). Pure ℝ[X] cancellation: μ(T−r) = μ(G−a)·Q ⟹ μ(G−a)·μ(T) = μ(G−a)·(μ(G)·Q), cancel μ(G−a).

theorem SimpleGraph.godsil_sum_prod_rearrange {ι : Type u_2} [Fintype ι] [DecidableEq ι] {R : Type u_3} [CommRing R] (μGu : R) (d s t : ι → R) (hIH : ∀ (b : ι), μGu * s b = d b * t b) : μGu * ∑ b : ι, s b * ∏ b' ∈ Finset.univ.erase b, t b' = (∑ b : ι, d b) * ∏ b : ι, t b

The Σ/∏ rearrangement at the inductive step of Godsil's identity. Indexing over the neighbours b ∼ u, write μGu = μ(G−u), d b = μ((G−u)−b), t b = μ(T(G−u,b)) and s b = μ(T(G−u,b) − r_b). Given the per-neighbour inductive hypothesis μGu · s b = d b · t b (Godsil's identity on the smaller graph G−u at b), the tree-side sum μGu · Σ_b s b·∏_{b'≠b} t b' collapses to (Σ_b d b)·∏_b t b — exactly what equates the tree recurrence's defect term with the G recurrence's after the root decomposition (D). Each summand: μGu·(s b·∏_{≠b} t) = (d b·t b)·∏_{≠b} t = d b·∏_all t via mul_prod_erase.

The partition function of the empty graph

theorem SimpleGraph.matchingPartition_bot {V : Type u_1} [Fintype V] : ⊥.matchingPartition = 1

P(⊥) = 1: the edgeless graph has only the empty matching. The base of the edge-count induction for Heilmann–Lieb.

theorem SimpleGraph.matchingPartition_bot_realRooted {V : Type u_1} [Fintype V] : MSS.RealRooted ⊥.matchingPartition

Base case of Heilmann–Lieb. P(⊥) = 1 is real-rooted (a nonzero constant splits trivially). The induction (on edge count, via matchingPartition_recurrence) builds from here.