Finiteness of Marchal states

A leaf-labelled tree with n + 1 leaves and no degree-two vertex has at most 2 * n vertices. Encoding its vertices by an initial segment therefore puts all representatives, and hence their quotient, in a finite type.

theorem BGW.StableTrees.Marchal.LTree.m_le_two_mul {n : ℕ} (T : LTree n) : T.m ≤ 2 * n

The vertex bound for a tree with n + 1 leaves and no degree-two vertices.

theorem BGW.StableTrees.Marchal.finite_state (n : ℕ) : Finite (State n)

The states are finitely many.