Boundary separation for the collapse step

For an eligible branch r, every point inside its subtree is much closer to the chosen inside representative than to any outside point. The strong quarter-distance form below is the geometric input needed to charge each changed boundary edge by 2; the weaker printed comparison (5.41) alone would not retain the paper's final 4^n ledger.

theorem Anderson4D.lcaPath_prefix_of_prefix_not_prefix {r p q : List ℕ} (hp : r <+: p) (hq : ¬r <+: q) : lcaPath p q <+: r

If r is a prefix of p but not of q, the longest common prefix of p and q is a prefix of r.

theorem Anderson4D.prefix_dropLast_of_prefix_ne {p q : List ℕ} (hpq : p <+: q) (hne : p ≠ q) : p <+: q.dropLast

A proper prefix remains a prefix after deleting the final entry of the longer path.

theorem Anderson4D.lcaV_ancestor_parent_of_prefix_not_prefix {t : PlaneTree} {r x y : t.VPos} (hx : ↑r <+: ↑x) (hy : ¬↑r <+: ↑y) : IsAncestor (lcaV x y) (PlaneTree.parentV r)

The LCA of an inside and an outside vertex is an ancestor of the parent of the collapsed root.

theorem Anderson4D.parentScale_le_lcaScale_of_inside_outside {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) {r : t.VPos} (hr : CollapseEligible Nm mu r) {l y : HeppLeaf t} (hl : l ∈ leavesUnder r) (hy : y ∉ leavesUnder r) : scaleN Nm (PlaneTree.parentV r) ≤ scaleN Nm (lcaV ↑l ↑y)

The parent scale of an eligible collapsed root is no larger than the LCA scale of an inside/outside pair.

theorem Anderson4D.eligible_boundary_quarter {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) {l lstar y : HeppLeaf t} (hl : l ∈ leavesUnder r) (hlstar : lstar ∈ leavesUnder r) (hy : y ∉ leavesUnder r) : 4 * znorm (z l - z lstar) ≤ znorm (z y - z l)

Strong boundary estimate behind (5.41): 4 |z_l-z_l*| ≤ |z_y-z_l|.

theorem Anderson4D.eligible_boundary_comparable {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) {l lstar y : HeppLeaf t} (hl : l ∈ leavesUnder r) (hlstar : lstar ∈ leavesUnder r) (hy : y ∉ leavesUnder r) : znorm (z y - z l) ≤ 2 * znorm (z y - z lstar) ∧ znorm (z y - z lstar) ≤ 2 * znorm (z y - z l)

Paper's weak two-sided comparison (5.41), derived from the strong quarter estimate and retained as a tree-facing corollary.