Pruning after placing the new leaf last

The degree-three case suppresses the penultimate vertex and restores the edge between its other two neighbours.

def BGW.StableTrees.Marchal.restrictLabels {n m M : ℕ} (f : Fin (n + 2) ↪ Fin M) (h : ∀ (i : Fin (n + 1)), ↑(f i.castSucc) < m) : Fin (n + 1) ↪ Fin m

Restrict old labels to a smaller initial segment containing them.

Equations

• BGW.StableTrees.Marchal.restrictLabels f h = { toFun := fun (i : Fin (n + 1)) => ⟨↑(f i.castSucc), ⋯⟩, inj' := ⋯ }

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

Canonical degree-three pruning gives a labelled parent.