Branch count away from a distinguished leaf

The factorial ledger in the collapse step of Proposition 5.9 needs the off-marker inequality 2 |W| ≤ m, where W is a set of non-root branch vertices and m is the total multiplicity of all leaves except the newly created marker leaf.

For a valid tree, the branch-excess Euler identity bounds the number of branch vertices by the number of leaves minus one. Erasing the root from the branch set and the marker from the leaf set, together with the lower bound two on every leaf multiplicity, gives the required estimate.

theorem Anderson4D.two_mul_card_nonrootBranches_le_sum_leafMultiplicity_erase {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (marker : HeppLeaf t) : 2 * (nonrootBranches t).card ≤ ∑ l ∈ Finset.univ.erase marker, leafMultiplicity mu l

Twice the number of non-root branch vertices is bounded by the total multiplicity away from any distinguished leaf.

theorem Anderson4D.two_mul_card_le_sum_leafMultiplicity_erase_of_subset_nonrootBranches {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (marker : HeppLeaf t) (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : 2 * W.card ≤ ∑ l ∈ Finset.univ.erase marker, leafMultiplicity mu l

Off-marker branch bound for an arbitrary subset of the non-root branch vertices. This is the form used by the factorial estimate (5.47).