Every Marchal state has a parent

Two swaps put the newest leaf and its neighbour last. The neighbour has degree at least three, so one of the two canonical pruning constructions applies.

theorem BGW.StableTrees.Marchal.LTree.leaf_neighbor_internal {k : ℕ} (T : LTree (k + 2)) (u : Fin T.m) (hadj : T.G.Adj (T.labels (Fin.last (k + 2))) u) : 3 ≤ T.G.degree u

The neighbour of a leaf in a tree with at least three labels is internal.

theorem BGW.StableTrees.Marchal.exists_graft_parent {k : ℕ} (T : LTree (k + 2)) : ∃ (S : LTree (k + 1)) (p : Position S.G), ⟦graft S p⟧ = ⟦T⟧

Every tree with at least three labelled leaves is a graft of a smaller labelled tree.

theorem BGW.StableTrees.Marchal.exists_graft_state (k : ℕ) (s : State (k + 2)) : ∃ (T : LTree (k + 1)) (p : Position T.G), ⟦graft T p⟧ = s

Grafting is surjective onto the next quotient state space.