Nonempty leaf carriers in the subtree-collapse step

The collapse coordinates use the sum alphabet InsideLeaf r ⊕ OutsideLeaf r. For a proper subtree of a tree whose root branches, both summands are inhabited. This file proves that structural fact and records the elementary occurrence consequence of membership in validWords.

theorem Anderson4D.two_le_leafCount_of_root_mem_BranchNodes (t : PlaneTree) (hroot : t.rootV ∈ t.BranchNodes) : 2 ≤ t.leafCount

A tree whose root is a branch node has at least two leaves.

theorem Anderson4D.root_mem_BranchNodes_contractAt_of_ne {t : PlaneTree} (r : t.VPos) (hr : r ≠ t.rootV) (hroot : t.rootV ∈ t.BranchNodes) : (t.contractAt ↑r).rootV ∈ (t.contractAt ↑r).BranchNodes

Contracting a proper rooted subtree preserves the branching root of the ambient tree.

theorem Anderson4D.nonempty_insideLeaf {t : PlaneTree} (r : t.VPos) : Nonempty (InsideLeaf r)

Every rooted subtree contains an original leaf below its root.

theorem Anderson4D.nonempty_outsideLeaf_of_ne_root {t : PlaneTree} (r : t.VPos) (hr : r ≠ t.rootV) (hroot : t.rootV ∈ t.BranchNodes) : Nonempty (OutsideLeaf r)

A proper rooted subtree of a tree whose root branches leaves at least one original leaf outside it.

theorem Anderson4D.exists_eq_of_mem_validWords_of_pos {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (mult : α → ℕ) (w : Fin M → α) (hw : w ∈ validWords mult) (a : α) (ha : 0 < mult a) : ∃ (i : Fin M), w i = a

A positive prescribed multiplicity forces the corresponding letter to occur in every valid word.