Rigidity of leaf-labelled trees

A longest extension of a path from the root ends at a leaf. An automorphism fixing all leaves fixes this path pointwise by uniqueness of paths in a tree.

theorem BGW.StableTrees.Marchal.LTree.iso_apply_eq {n : ℕ} (T : LTree n) (e : T.G ≃g T.G) (he : ∀ (i : Fin (n + 1)), e (T.labels i) = T.labels i) (v : Fin T.m) : e v = v

Every automorphism fixing the leaf labels fixes every vertex.

theorem BGW.StableTrees.Marchal.graft_state_injective {n : ℕ} (T : LTree n) : Function.Injective fun (p : Position T.G) => ⟦graft T p⟧

Two positions in a leaf-labelled tree give distinct graft states.