Branch-cardinality ledger for subtree contraction

The branch set of the original tree is partitioned exactly into branches inside the collapsed subtree and branches retained by the contracted tree. This supplies the strict D-power saving in (5.45).

def Anderson4D.branchesOutsideEquivFilter {t : PlaneTree} (r : t.VPos) : t.BranchesOutside ↑r ≃ ↥({u ∈ t.BranchNodes | ¬↑r <+: ↑u})

Branch vertices outside the subtree, as an ordinary filtered subtype.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.descendantBranchesEquivBranchNodesUnder {t : PlaneTree} (r : t.VPos) : PlaneTree.DescendantBranches r ≃ ↥(branchNodesUnder r)

Descendant branches, as the subtype of branchNodesUnder r.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.card_branchesOutside_eq_filter {t : PlaneTree} (r : t.VPos) : Fintype.card (t.BranchesOutside ↑r) = {u ∈ t.BranchNodes | ¬↑r <+: ↑u}.card

theorem Anderson4D.card_descendantBranches_eq_branchNodesUnder {t : PlaneTree} (r : t.VPos) : Fintype.card (PlaneTree.DescendantBranches r) = (branchNodesUnder r).card

theorem Anderson4D.card_BranchNodes_contractAt_add_card_BranchNodes_subtreeAt {t : PlaneTree} (r : t.VPos) : (t.contractAt ↑r).BranchNodes.card + (t.subtreeAt ↑r).BranchNodes.card = t.BranchNodes.card

Exact branch partition under contraction.

theorem Anderson4D.card_BranchNodes_contractAt_add_one_le {t : PlaneTree} {r : t.VPos} (hr : r ∈ t.BranchNodes) : (t.contractAt ↑r).BranchNodes.card + 1 ≤ t.BranchNodes.card

Contracting a branch removes at least that branch from the branch count. This is the exponent inequality used to extract one factor D⁻¹.

theorem Anderson4D.card_BranchNodes_contractAt_le_sub_one {t : PlaneTree} {r : t.VPos} (hr : r ∈ t.BranchNodes) : (t.contractAt ↑r).BranchNodes.card ≤ t.BranchNodes.card - 1

Subtractive form of the same strict branch saving.