Tree structure before grafting

Connectivity can be pulled back through an edge graft by collapsing both new vertices onto one endpoint of the subdivided edge. The degree sum then recovers the tree edge count.

theorem BGW.StableTrees.Marchal.isTree_of_graftGraph_inl {m : ℕ} (G : SimpleGraph (Fin m)) (e : ↑G.edgeSet) (hG : (graftGraph G (Sum.inl e)).IsTree) : G.IsTree

If an edge graft is a tree, its parent graph is a tree.

def BGW.StableTrees.Marchal.edgePruneGraph {m : ℕ} (G : SimpleGraph (Fin (m + 2))) (a b : Fin m) : SimpleGraph (Fin m)

Delete the two last vertices and restore the edge between a and b.

Equations

• BGW.StableTrees.Marchal.edgePruneGraph G a b = SimpleGraph.comap (fun (x : Fin m) => x.castSucc.castSucc) G ⊔ SimpleGraph.fromEdgeSet {s(a, b)}

def BGW.StableTrees.Marchal.edgePrunePosition {m : ℕ} (G : SimpleGraph (Fin (m + 2))) (a b : Fin m) (hab : a ≠ b) : ↑(edgePruneGraph G a b).edgeSet

The restored edge in the pruned graph.

Equations

• BGW.StableTrees.Marchal.edgePrunePosition G a b hab = ⟨s(a, b), ⋯⟩

theorem BGW.StableTrees.Marchal.graftGraph_edgePruneGraph {m : ℕ} (G : SimpleGraph (Fin (m + 2))) (a b : Fin m) (hab : a ≠ b) (hnew : ∀ (x : Fin (m + 2)), G.Adj (Fin.last (m + 1)) x ↔ x = (Fin.last m).castSucc) (hmid : ∀ (x : Fin m), G.Adj (Fin.last m).castSucc x.castSucc.castSucc ↔ x = a ∨ x = b) (hnot : ¬G.Adj a.castSucc.castSucc b.castSucc.castSucc) : graftGraph (edgePruneGraph G a b) (Sum.inl (edgePrunePosition G a b hab)) = G

Grafting after explicit deletion and suppression recovers the original graph.

theorem BGW.StableTrees.Marchal.edgePruneGraph_isTree {m : ℕ} (G : SimpleGraph (Fin (m + 2))) (hG : G.IsTree) (a b : Fin m) (hab : a ≠ b) (hnew : ∀ (x : Fin (m + 2)), G.Adj (Fin.last (m + 1)) x ↔ x = (Fin.last m).castSucc) (hmid : ∀ (x : Fin m), G.Adj (Fin.last m).castSucc x.castSucc.castSucc ↔ x = a ∨ x = b) (hnot : ¬G.Adj a.castSucc.castSucc b.castSucc.castSucc) : (edgePruneGraph G a b).IsTree

Explicit deletion and suppression of a terminal cherry preserves the tree property.