Godsil's identity for the path tree

Removing the root r from the path tree T(G, u) leaves the disjoint union of the path trees T(G - u, b) over the neighbours b of u. Together with the vertex-deletion recurrence of the matching polynomial this gives, by induction on the number of edges, Godsil's identity μ(G) · μ(T(G, u) - r) = μ(G - u) · μ(T(G, u)).

Main definitions

• SimpleGraph.dropRoot: the inverse of prependRoot on non-root paths.
• SimpleGraph.rootDecompEquiv, SimpleGraph.rootDecompIso: the vertex bijection and the graph isomorphism T(G, u) - r ≃g ⊥ ⊕ ⨆_{b ∼ u} T(G - u, b).

Main results

• SimpleGraph.matchingPoly_pathTree_deleteRoot: μ(T(G, u) - r) = X · ∏_{b ∼ u} μ(T(G - u, b)).
• SimpleGraph.godsil_identity: μ(G) · μ(T(G, u) - r) = μ(G - u) · μ(T(G, u)).

Here G - u is G.deleteIncidenceSet u: the vertex u is kept, isolated, which multiplies the matching polynomial by X.

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.

The root decomposition T(G,u) − r ≅ ⊔_{b∼u} T(G−u,b): the inverse dropRoot

theorem SimpleGraph.dropRoot_aux {V : Type u_1} {G : SimpleGraph V} {u : V} (p : G.PathFrom u) (hp : ¬(↑p.snd).Nil) (e : Sym2 V) : e ∈ (↑p.snd).tail.edges → e ∈ (G.deleteIncidenceSet u).edgeSet

The tail of a non-root path of T(G,u) has all its edges in G−u (it avoids u).

def SimpleGraph.dropRoot {V : Type u_1} {G : SimpleGraph V} {u : V} (p : G.PathFrom u) (hp : ¬(↑p.snd).Nil) : (G.deleteIncidenceSet u).PathFrom (↑p.snd).snd

Inverse of prependRoot. Drop the root edge from a non-root path of T(G,u): its Walk.tail is a path of G−u from the second vertex (the tail avoids u, which appears only at the head of the original path, so every tail edge survives in G−u).

Equations

• SimpleGraph.dropRoot p hp = ⟨p.fst, ⟨(↑p.snd).tail.transfer (G.deleteIncidenceSet u) ⋯, ⋯⟩⟩

theorem SimpleGraph.mapLe_transfer_self {V : Type u_1} {G H : SimpleGraph V} (hle : H ≤ G) {a b : V} (w : G.Walk a b) (h : ∀ e ∈ w.edges, e ∈ H.edgeSet) : Walk.mapLe hle (w.transfer H h) = w

mapLe of a transfer into the supergraph is the identity walk (both = transfer into that graph, via transfer_eq_map_ofLE + transfer_transfer + transfer_self).

theorem SimpleGraph.prependRoot_dropRoot {V : Type u_1} {G : SimpleGraph V} {u : V} (p : G.PathFrom u) (hp : ¬(↑p.snd).Nil) : G.prependRoot ⋯ (dropRoot p hp) = p

prependRoot ∘ dropRoot = id: re-attaching the root edge recovers the original path.

theorem SimpleGraph.prependRoot_not_nil {V : Type u_1} {G : SimpleGraph V} {u b : V} (hub : G.Adj u b) (q : (G.deleteIncidenceSet u).PathFrom b) : ¬(↑(G.prependRoot hub q).snd).Nil

An image of prependRoot is never the root (it starts with the root edge).

theorem SimpleGraph.pathFrom_eq_root_of_nil {V : Type u_1} {G : SimpleGraph V} {u : V} (p : G.PathFrom u) (hp : (↑p.snd).Nil) : p = G.pathTreeRoot u

A path of T(G,u) whose walk is Nil is the root.

@[simp]

theorem SimpleGraph.prependRoot_snd {V : Type u_1} {G : SimpleGraph V} {u b : V} (hub : G.Adj u b) (q : (G.deleteIncidenceSet u).PathFrom b) : (↑(G.prependRoot hub q).snd).snd = b

The second vertex of prependRoot G hub q is b (the root edge's far end).

theorem SimpleGraph.prependRoot_heq_inj {V : Type u_1} {G : SimpleGraph V} {u b₁ b₂ : V} (h₁ : G.Adj u b₁) (h₂ : G.Adj u b₂) {x : (G.deleteIncidenceSet u).PathFrom b₁} {y : (G.deleteIncidenceSet u).PathFrom b₂} (h : G.prependRoot h₁ x = G.prependRoot h₂ y) : x ≍ y

prependRoot is injective even across the far endpoint (HEq). Equal images force equal second vertices (prependRoot_snd), and once those are identified (b₁, b₂ are free here, so subst works — this is what dissolves the b ∈ snd circularity), it is the ordinary injectivity of prependRoot (the root-edge proof is irrelevant).

theorem SimpleGraph.dropRoot_prependRoot {V : Type u_1} {G : SimpleGraph V} {u b : V} (hub : G.Adj u b) (q : (G.deleteIncidenceSet u).PathFrom b) : dropRoot (G.prependRoot hub q) ⋯ ≍ q

dropRoot ∘ prependRoot = id (the second round-trip, HEq): prependRoot_dropRoot re-attaches the dropped root edge to give back prependRoot q, and prependRoot_heq_inj cancels the outer prependRoot.

theorem SimpleGraph.prependRoot_walk {V : Type u_1} {G : SimpleGraph V} {u b : V} (hub : G.Adj u b) (q : (G.deleteIncidenceSet u).PathFrom b) : ↑(G.prependRoot hub q).snd = Walk.cons hub (Walk.mapLe ⋯ ↑q.snd)

The walk underlying prependRoot (definitionally a cons of the root edge).

theorem SimpleGraph.Grows_snd_eq {V : Type u_1} {G : SimpleGraph V} {u : V} {a b : G.PathFrom u} (h : Grows a b) (ha : ¬(↑a.snd).Nil) : (↑a.snd).snd = (↑b.snd).snd

Grows preserves the second vertex: if b extends a (non-root) by one edge at the end, they share the same first step.

theorem SimpleGraph.pathTree_adj_prependRoot {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u b₁ b₂ : V} (h₁ : G.Adj u b₁) (h₂ : G.Adj u b₂) (x : (G.deleteIncidenceSet u).PathFrom b₁) (y : (G.deleteIncidenceSet u).PathFrom b₂) : (G.pathTree u).Adj (G.prependRoot h₁ x) (G.prependRoot h₂ y) ↔ (sigmaFamily fun (b : { b : V // G.Adj u b }) => (G.deleteIncidenceSet u).pathTree ↑b).Adj ⟨⟨b₁, h₁⟩, x⟩ ⟨⟨b₂, h₂⟩, y⟩

Per-fibre adjacency of the path tree under prependRoot. Two branch paths are adjacent in T(G,u) iff they sit in the same fibre and are adjacent in T(G−u, b) — i.e. exactly the adjacency of the indexed disjoint union. Same trick as prependRoot_heq_inj: b₁, b₂ are FREE, so the same-fibre case substs cleanly (prependRoot_grows), and the cross-fibre case is impossible (Grows preserves the second vertex, snd_cons).

noncomputable def SimpleGraph.rootDecompEquiv {V : Type u_1} (G : SimpleGraph V) (u : V) : G.PathFrom u ≃ Unit ⊕ (b : { b : V // G.Adj u b }) × (G.deleteIncidenceSet u).PathFrom ↑b

Root-decomposition vertex equivalence. A path of T(G,u) is either the root or a path u-prepended to a path of G−u from a neighbour b. So PathFrom G u ≃ Unit ⊕ Σ b:{b // u∼b}, PathFrom (G−u) b. Forward = case on Nil (root ↦ inl, else ↦ dropRoot); inverse = root / prependRoot. The two round-trips prependRoot_dropRoot (Eq) and dropRoot_prependRoot (HEq) supply the inverses.

Equations

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

noncomputable def SimpleGraph.rootDecompIso {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (u : V) : (G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u) ≃g ⊥ ⊕g sigmaFamily fun (b : { b : V // G.Adj u b }) => (G.deleteIncidenceSet u).pathTree ↑b

Root-decomposition graph isomorphism. T(G,u) − r ≃g (⊥ on the root) ⊕ ⊔_{b∼u} T(G−u,b). The vertex part is rootDecompEquiv; adjacency: the root is isolated (in deleteIncidenceSet and in ⊥ Unit / across the sum), and branch adjacency is exactly pathTree_adj_prependRoot.

Equations

• G.rootDecompIso u = { toEquiv := G.rootDecompEquiv u, map_rel_iff' := ⋯ }

theorem SimpleGraph.matchingPoly_bot_sum_sigmaFamily {ι : Type u_2} [Fintype ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (H : (i : ι) → SimpleGraph (β i)) : (⊥ ⊕g sigmaFamily H).matchingPoly = Polynomial.X * ∏ i : ι, (H i).matchingPoly

μ of (⊥ on a point) ⊕ ⊔_i H_i is X · ∏_i μ(H_i). Proved in a clean context (no graph iso), so matchingPoly_sigmaFamily applies on the direct Σ-Fintype with no instance diamond.

theorem SimpleGraph.matchingPoly_bot_sum_sigmaFamily_delete {ι : Type u_2} [Fintype ι] [DecidableEq ι] {β : ι → Type u_3} [(i : ι) → Fintype (β i)] (H : (i : ι) → SimpleGraph (β i)) (b : ι) (y : β b) : ((⊥ ⊕g sigmaFamily H).deleteIncidenceSet (Sum.inr ⟨b, y⟩)).matchingPoly = Polynomial.X * ((H b).deleteIncidenceSet y).matchingPoly * ∏ i ∈ Finset.univ.erase b, (H i).matchingPoly

μ of (⊥ on a point) ⊕ ⊔_i H_i with one fibre-b vertex ⟨b,y⟩ deleted is X · μ(H_b − y) · ∏_{i≠b} μ(H_i). Clean context (no graph iso): sumDeleteIncidenceSetInr isolates the right summand, sigmaFamilyDelete replaces the b-fibre by H_b − y, and matchingPoly_sigmaFamily + prod_update evaluate the product. The evaluation half of the () sub-decomposition μ(T−r−c_b) = X·μ(T_b−r_b)·∏_{b'≠b} μ(T_b').

theorem SimpleGraph.matchingPoly_pathTree_deleteRoot {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [(b : { b : V // G.Adj u b }) → Fintype ((G.deleteIncidenceSet u).PathFrom ↑b)] : ((G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u)).matchingPoly = Polynomial.X * ∏ b : { b : V // G.Adj u b }, ((G.deleteIncidenceSet u).pathTree ↑b).matchingPoly

(D) — the root-decomposition matching-polynomial identity. μ(T(G,u) − r) = X · ∏_{b∼u} μ(T(G−u, b)). Chains the two proven halves — matchingPoly_iso (rootDecompIso G u) : μ(T−r) = μ[(⊥)⊕⊔_b T(G−u,b)] (the graph iso) and matchingPoly_bot_sum_sigmaFamily : μ[(⊥)⊕⊔_b H_b] = X·∏ μ(H_b) (the evaluation). convert matches the two structurally up to depth 2 and discharges the leftover Fintype/Decidable instance mismatches (the Σ-type diamond) via Subsingleton.elim — sidestepping the whnf-reduction of μ over the Σ-type that blows the heartbeat budget on a direct chain.

Piece 2 of (): the root's neighbours are the children prependRoot of b ∼ u

theorem SimpleGraph.pathTree_root_adj_iff {V : Type u_1} (G : SimpleGraph V) (u : V) (c : G.PathFrom u) : (G.pathTree u).Adj (G.pathTreeRoot u) c ↔ ∃ (b : V) (h : G.Adj u b), c = G.prependRoot h ((G.deleteIncidenceSet u).pathTreeRoot b)

A path is adjacent to the root iff it is a single edge u → b. Grows c r is impossible (a concat is never nil), so the only neighbours of r are the length-one paths, i.e. prependRoot of the trivial path of G−u at a neighbour b ∼ u. The index b is kept free (not c.1) so the backward direction can subst.

theorem SimpleGraph.prependRoot_root_injective {V : Type u_1} (G : SimpleGraph V) (u : V) : Function.Injective fun (b : { b : V // G.Adj u b }) => G.prependRoot ⋯ ((G.deleteIncidenceSet u).pathTreeRoot ↑b)

The child map b ↦ (u → b) is injective: the path's endpoint recovers b.

theorem SimpleGraph.pathTreeRoot_neighborFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [DecidableRel (G.pathTree u).Adj] : (G.pathTree u).neighborFinset (G.pathTreeRoot u) = Finset.image (fun (b : { b : V // G.Adj u b }) => G.prependRoot ⋯ ((G.deleteIncidenceSet u).pathTreeRoot ↑b)) Finset.univ

The root's neighbour set is the image of b ∼ u under the child embedding.

theorem SimpleGraph.sum_root_neighbors {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_2} [AddCommMonoid M] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [DecidableRel (G.pathTree u).Adj] (F : G.PathFrom u → M) : ∑ c ∈ (G.pathTree u).neighborFinset (G.pathTreeRoot u), F c = ∑ b : { b : V // G.Adj u b }, F (G.prependRoot ⋯ ((G.deleteIncidenceSet u).pathTreeRoot ↑b))

Reindex a sum over the root's neighbours by b ∼ u (the form the tree recurrence needs in ()).

def SimpleGraph.matchingPoly_pathTree_deleteRoot_child_target {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [(b : { b : V // G.Adj u b }) → Fintype ((G.deleteIncidenceSet u).PathFrom ↑b)] (b : { b : V // G.Adj u b }) : Prop

() sub-decomposition. μ(T(G,u) − r − c_b) = X · μ(T(G−u,b) − r_b) · ∏_{b'≠b} μ(T(G−u,b')) for the child c_b = prependRoot G b.2 r_b = (u → b). The math is settled: c_b ↦ inr ⟨b, r_b⟩ under rootDecompEquiv, and matchingPoly_bot_sum_sigmaFamily_delete (proven) evaluates the image. The gap is transporting μ across (rootDecompIso).deleteIncidenceSet c_b: matchingPoly_iso/matchingNumber_iso of the doubly-deleted Σ-of-paths graph blows the whnf/isDefEq budget. RESISTS every tactic-level fix tried (1M/4M/16M heartbeats; the simple-codomain ▸; the general wrapper matchingPoly_deleteIncidenceSet_iso; the Socratic free-vertex abstraction). Unlike the HEq wall (logical), this is pure elaboration cost: passing the complex iso rootDecompIso to the transport triggers it regardless. Fix needs either a whnf-free reproof of matchingNumber_iso, or the Herglotz/u = 1/R route (avoids the path tree entirely).

Equations

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

theorem SimpleGraph.matchingPoly_pathTree_deleteRoot_child {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [(b : { b : V // G.Adj u b }) → Fintype ((G.deleteIncidenceSet u).PathFrom ↑b)] (b : { b : V // G.Adj u b }) : G.matchingPoly_pathTree_deleteRoot_child_target u b

() sub-decomposition (the formerly whnf-blocked child_target). The vertex c_b = prependRoot G b.2 r_b maps under rootDecompIso to Sum.inr ⟨b, r_b⟩ — this is exactly rootDecompEquiv's apply_symm_apply (since rootDecompEquiv.symm (inr ⟨b,r_b⟩) = prependRoot … by rfl). The general transport matchingPoly_deleteIncidenceSet_iso (rootDecompIso G u) c_b moves μ to the (⊥)⊕sigmaFamily side. The KEY to dodge the whnf wall: do NOT cite matchingPoly_bot_sum_sigmaFamily_delete (that forces unifying the transport-produced Σ-graph with the lemma's Σ-graph — a whnf loop over the path Fintype). Instead INLINE its proof (sumDeleteIncidenceSetInr → sigmaFamilyDeleteIncidenceSet → matchingPoly_sigmaFamily), rewriting the goal's own graph term in place — no second graph, no unification.

theorem SimpleGraph.godsil_identity_step {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) [Fintype (G.PathFrom u)] [(b : { b : V // G.Adj u b }) → Fintype ((G.deleteIncidenceSet u).PathFrom ↑b)] (IH : ∀ (b : { b : V // G.Adj u b }), (G.deleteIncidenceSet u).matchingPoly * (((G.deleteIncidenceSet u).pathTree ↑b).deleteIncidenceSet ((G.deleteIncidenceSet u).pathTreeRoot ↑b)).matchingPoly = ((G.deleteIncidenceSet u).deleteIncidenceSet ↑b).matchingPoly * ((G.deleteIncidenceSet u).pathTree ↑b).matchingPoly) (hchild : ∀ (b : { b : V // G.Adj u b }), (((G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u)).deleteIncidenceSet (G.prependRoot ⋯ ((G.deleteIncidenceSet u).pathTreeRoot ↑b))).matchingPoly = Polynomial.X * (((G.deleteIncidenceSet u).pathTree ↑b).deleteIncidenceSet ((G.deleteIncidenceSet u).pathTreeRoot ↑b)).matchingPoly * ∏ b' ∈ Finset.univ.erase b, ((G.deleteIncidenceSet u).pathTree ↑b').matchingPoly) : G.matchingPoly * ((G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u)).matchingPoly = (G.deleteIncidenceSet u).matchingPoly * (G.pathTree u).matchingPoly

Godsil's identity — the inductive step (). Given the identity on G−u at every neighbour b (the IH), it holds for G at u. Cancel X² (a non-zero-divisor); expand the vertex-deletion recurrence at u in G and at the root r in the tree T; feed the root decomposition (D) μ(T−r)=X·∏ μ(T_b), the sub-decomposition of each tree-recurrence defect term μ(T−r−c_b)=X·μ(T_b−r_b)·∏_{b'≠b}μ(T_b'), and the Σ/∏ rearrangement godsil_sum_prod_rearrange fed by the IH; close by linear_combination.

def SimpleGraph.godsil_identity_target {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u : V) [Fintype (G.PathFrom u)] [DecidableRel (G.pathTree u).Adj] : Prop

Godsil's identity μ(G)·μ(T(G,u)−r) = μ(G−u)·μ(T(G,u)) — stated target. The induction is fully written and godsil_identity_step (the inductive step) is (strong induction on edge count: G−u has strictly fewer edges whenever u has a neighbour; Fintype (G.PathFrom u) synthesized from SimpleGraph.Path.instFintype + Sigma). The only missing input to the induction is matchingPoly_pathTree_deleteRoot_child_target (the whnf- blocked sub-decomposition hchild that godsil_identity_step takes as a hypothesis). Once that child target is discharged, godsil_identity_step + the written induction close this in full.

Equations

• G.godsil_identity_target u = (G.matchingPoly * ((G.pathTree u).deleteIncidenceSet (G.pathTreeRoot u)).matchingPoly = (G.deleteIncidenceSet u).matchingPoly * (G.pathTree u).matchingPoly)

@[instance_reducible]

noncomputable instance SimpleGraph.instFintypePathFrom {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (u : V) : Fintype (G.PathFrom u)

PathFrom u = Σ v, Path u v is a finite type (a def, so synthesis needs this explicit instance via Path.instFintype + Sigma). Registering it globally lets the edge-count induction synthesize all Fintype (· .PathFrom ·) arguments for the induced subgraphs G − u.

Equations

• G.instFintypePathFrom u = { elems := Finset.univ.sigma fun (x : V) => Finset.univ, complete := ⋯ }

@[instance_reducible]

noncomputable instance SimpleGraph.instDecidableRelPathTreeAdj {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (u : V) : DecidableRel (G.pathTree u).Adj

Canonical DecidableRel (pathTree.Adj). pathTree.Adj = Grows carries no structural Decidable instance, so it is decided Classically — but with no registered choice, each call synthesizes its own Classical.propDecidable, and the μ(pathTree) / μ(T−r) terms they build become syntactically distinct Subsingleton-equal instances, forcing a divergent whnf over the Σ-paths μ when the path-tree divisibility assembly meets godsil_identity/(D). Registering one choice (keyed on the pathTree.Adj head — no abbrev unfolding ambiguity) makes them agree.

Equations

• G.instDecidableRelPathTreeAdj u x✝¹ x✝ = Classical.propDecidable ((G.pathTree u).Adj x✝¹ x✝)

theorem SimpleGraph.godsil_identity {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (u : V) : G.godsil_identity_target u

Godsil's identity. μ(G)·μ(T(G,u)−r) = μ(G−u)·μ(T(G,u)), for every finite graph. Strong induction on the edge count: godsil_identity_step reduces it to the identity on G − u at each neighbour b ∼ u (the IH — G − u has strictly fewer edges, the edge {u,b} being gone) plus the now-proven child sub-decomposition matchingPoly_pathTree_deleteRoot_child.