Pruning a leaf at a vertex of degree at least four

Deleting the last leaf leaves its neighbour selectable as an internal vertex.

theorem BGW.StableTrees.Marchal.isTree_of_graftGraph_inr {m : ℕ} (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (hG : (graftGraph G (Sum.inr v)).IsTree) : G.IsTree

If a vertex graft is a tree, its parent graph is a tree.

theorem BGW.StableTrees.Marchal.exists_graft_inr_of_iso {n m : ℕ} (T : LTree (n + 1)) (G : SimpleGraph (Fin m)) (v : { v : Fin m // 3 ≤ G.degree v }) (e : graftGraph G (Sum.inr v) ≃g T.G) (f : Fin (n + 1) ↪ Fin m) (hold : ∀ (i : Fin (n + 1)), e (f i).castSucc = T.labels i.castSucc) (hnew : e (Fin.last m) = T.labels (Fin.last (n + 1))) : ∃ (S : LTree n) (p : Position S.G), ⟦graft S p⟧ = ⟦T⟧

A vertex-graft reconstruction with the right labels gives a labelled parent.

theorem BGW.StableTrees.Marchal.degree_comap_castSucc_add {m : ℕ} (G : SimpleGraph (Fin (m + 1))) (x : Fin m) : ((SimpleGraph.comap Fin.castSucc G).degree x + if G.Adj x.castSucc (Fin.last m) then 1 else 0) = G.degree x.castSucc

Deleting the last vertex removes exactly its possible incident edge at each old vertex.

theorem BGW.StableTrees.Marchal.exists_graft_vertex_canonical {n m : ℕ} (G : SimpleGraph (Fin (m + 1))) (tree : G.IsTree) (labels : Fin (n + 2) ↪ Fin (m + 1)) (leaf : ∀ (v : Fin (m + 1)), G.degree v = 1 ↔ v ∈ Set.range ⇑labels) (branch : ∀ (v : Fin (m + 1)), G.degree v ≠ 1 → 3 ≤ G.degree v) (hlast : labels (Fin.last (n + 1)) = Fin.last m) (u : Fin m) (hnew : ∀ (x : Fin m), G.Adj (Fin.last m) x.castSucc ↔ x = u) (hdegree : 4 ≤ G.degree u.castSucc) : ∃ (S : LTree n) (p : Position S.G), ⟦graft S p⟧ = ⟦{ m := m + 1, G := G, tree := tree, labels := labels, leaf := leaf, branch := branch }⟧

Canonical pruning at an old vertex of degree at least four gives a labelled parent.