Parents in valid Hepp trees

In a valid PlaneTree, every internal vertex is branching: unary vertices are excluded by PlaneTree.isValid. Consequently the parent of every non-root vertex is a branching vertex.

theorem Anderson4D.parentV_mem_BranchNodes_of_isValid {t : PlaneTree} (ht : t.isValid = true) {v : t.VPos} (hne : v ≠ t.rootV) : PlaneTree.parentV v ∈ t.BranchNodes

In a valid Hepp tree, the parent of every non-root vertex is branching. This is the general form used by marking monotonicity and automorphism arguments.

theorem Anderson4D.parentV_mem_BranchNodes_of_branch {t : PlaneTree} (ht : t.isValid = true) {v : t.VPos} (_hv : v ∈ t.BranchNodes) (hne : v ≠ t.rootV) : PlaneTree.parentV v ∈ t.BranchNodes

Paper-facing specialization: the parent of a non-root branching vertex in a valid Hepp tree is branching.