Transport of skipped branch sets through contraction

The induction hypothesis on the contracted tree sums over its non-root branch sets W. Equation (5.46) lifts such a set back to the original tree and, only when s = 1, inserts the collapsed branch r.

def Anderson4D.contractVertexEmbedding {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) : (t.contractAt p).VPos ↪ t.VPos

The retained-vertex inclusion as an embedding.

Equations

• Anderson4D.contractVertexEmbedding hp = { toFun := Anderson4D.PlaneTree.contractVertex hp, inj' := ⋯ }

def Anderson4D.liftContractFinset {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) (W : Finset (t.contractAt p).VPos) : Finset t.VPos

Lift a finite vertex set from the contracted tree to the original tree.

Equations

• Anderson4D.liftContractFinset hp W = Finset.map (Anderson4D.contractVertexEmbedding hp) W

@[simp]

theorem Anderson4D.card_liftContractFinset {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) (W : Finset (t.contractAt p).VPos) : (liftContractFinset hp W).card = W.card

@[simp]

theorem Anderson4D.mem_liftContractFinset_iff {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) (W : Finset (t.contractAt p).VPos) (v : t.VPos) : v ∈ liftContractFinset hp W ↔ ∃ w ∈ W, PlaneTree.contractVertex hp w = v

theorem Anderson4D.contractVertex_mem_nonrootBranches {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) {v : (t.contractAt p).VPos} (hv : v ∈ nonrootBranches (t.contractAt p)) : PlaneTree.contractVertex hp v ∈ nonrootBranches t

A contracted non-root branch lifts to an original non-root branch.

theorem Anderson4D.liftContractFinset_subset_nonrootBranches {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) {W : Finset (t.contractAt p).VPos} (hW : W ⊆ nonrootBranches (t.contractAt p)) : liftContractFinset hp W ⊆ nonrootBranches t

Lifting preserves the non-root-branch subset condition.

theorem Anderson4D.not_mem_liftContractFinset_of_subset_nonrootBranches {t : PlaneTree} (r : t.VPos) {W : Finset (t.contractAt ↑r).VPos} (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : r ∉ liftContractFinset ⋯ W

The collapsed root is not among the lifted contracted branches.

def Anderson4D.liftWPrime {t : PlaneTree} (r : t.VPos) (s : ℕ) (W : Finset (t.contractAt ↑r).VPos) : Finset t.VPos

Paper's set W': insert r exactly in the one-cut case.

Equations

• Anderson4D.liftWPrime r s W = if s = 1 then insert r (Anderson4D.liftContractFinset ⋯ W) else Anderson4D.liftContractFinset ⋯ W

theorem Anderson4D.card_liftWPrime {t : PlaneTree} (r : t.VPos) (s : ℕ) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : (liftWPrime r s W).card = if s = 1 then W.card + 1 else W.card

Exact cardinality ledger for W ↦ W'.

theorem Anderson4D.liftWPrime_subset_nonrootBranches {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) {W : Finset (t.contractAt ↑r).VPos} (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : liftWPrime r s W ⊆ nonrootBranches t

The lifted set is a valid original non-root branch set whenever the collapsed root itself is non-root.