Subtrees and contractions of plane Hepp trees

This file provides the structural API used by the collapse induction in paper §5.4.1. Positions in a PlaneTree are paths from the root, so the subtree at a valid position is obtained by following that path. Contracting at a position replaces the whole rooted subtree there by one leaf.

The API is deliberately independent of markings, multiplicities, and embeddings. Those data are transported in the later collapse layers.

The rooted subtree at a position

def Anderson4D.PlaneTree.subtreeAt : PlaneTree → Pos → PlaneTree

The subtree rooted at p. At an invalid position this returns the bare leaf; all mathematical uses supply IsPos t p, under which the fallback is unreachable.

Equations

• x✝.subtreeAt [] = x✝
• (Anderson4D.PlaneTree.node cs).subtreeAt (i :: p) = if h : i < cs.length then cs[i].subtreeAt p else Anderson4D.PlaneTree.leaf

@[simp]

theorem Anderson4D.PlaneTree.subtreeAt_nil (t : PlaneTree) : t.subtreeAt [] = t

theorem Anderson4D.PlaneTree.subtreeAt_cons_of_lt {cs : List PlaneTree} {i : ℕ} {p : Pos} (hi : i < cs.length) : (node cs).subtreeAt (i :: p) = cs[i].subtreeAt p

theorem Anderson4D.PlaneTree.isPos_subtreeAt_iff {t : PlaneTree} {p q : Pos} (hp : t.IsPos p) : (t.subtreeAt p).IsPos q ↔ t.IsPos (p ++ q)

A path q is valid in the rooted subtree at p exactly when p ++ q is valid in the original tree.

theorem Anderson4D.PlaneTree.childCount_subtreeAt {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (q : Pos) : (t.subtreeAt p).childCount q = t.childCount (p ++ q)

Child counts are unchanged when a vertex is viewed inside a rooted subtree.

theorem Anderson4D.PlaneTree.isValid_subtreeAt {t : PlaneTree} {p : Pos} (ht : t.isValid = true) (hp : t.IsPos p) : (t.subtreeAt p).isValid = true

A rooted subtree of a valid Hepp tree is valid.

theorem Anderson4D.PlaneTree.subtreeAt_size_le {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.subtreeAt p).size ≤ t.size

A rooted subtree never has more vertices than the original tree.

theorem Anderson4D.PlaneTree.subtreeAt_size_lt {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (hp0 : p ≠ []) : (t.subtreeAt p).size < t.size

Every proper rooted subtree (one whose root is not the original root) has strictly fewer vertices. This is the well-founded measure for the collapse induction.

Vertex, leaf, and branch transport

@[reducible, inline]

abbrev Anderson4D.PlaneTree.Descendants {t : PlaneTree} (r : t.VPos) : Type

Vertices of t lying weakly below r.

Equations

• Anderson4D.PlaneTree.Descendants r = { v : t.VPos // ↑r <+: ↑v }

def Anderson4D.PlaneTree.subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : t.VPos

Include a vertex of the subtree at r into the original tree by prepending r's path.

Equations

• Anderson4D.PlaneTree.subtreeVertex r v = ⟨↑r ++ ↑v, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.subtreeVertex_val {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : ↑(subtreeVertex r v) = ↑r ++ ↑v

theorem Anderson4D.PlaneTree.subtreeVertex_injective {t : PlaneTree} (r : t.VPos) : Function.Injective (subtreeVertex r)

@[simp]

theorem Anderson4D.PlaneTree.subtreeVertex_root {t : PlaneTree} (r : t.VPos) : subtreeVertex r (t.subtreeAt ↑r).rootV = r

def Anderson4D.PlaneTree.subtreeVertexEquiv {t : PlaneTree} (r : t.VPos) : (t.subtreeAt ↑r).VPos ≃ Descendants r

Vertices of the rooted subtree are exactly descendants of its root in the original tree.

Equations

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

@[simp]

theorem Anderson4D.PlaneTree.subtreeVertexEquiv_apply_val {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : ↑((subtreeVertexEquiv r) v) = subtreeVertex r v

theorem Anderson4D.PlaneTree.childCount_subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : (t.subtreeAt ↑r).childCount ↑v = t.childCount ↑(subtreeVertex r v)

Child count is preserved by the subtree vertex inclusion.

theorem Anderson4D.PlaneTree.mem_Leaves_subtreeVertex_iff {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : v ∈ (t.subtreeAt ↑r).Leaves ↔ subtreeVertex r v ∈ t.Leaves

theorem Anderson4D.PlaneTree.mem_BranchNodes_subtreeVertex_iff {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : v ∈ (t.subtreeAt ↑r).BranchNodes ↔ subtreeVertex r v ∈ t.BranchNodes

@[reducible, inline]

abbrev Anderson4D.PlaneTree.DescendantLeaves {t : PlaneTree} (r : t.VPos) : Type

Leaves of t below r, represented as descendant vertices.

Equations

• Anderson4D.PlaneTree.DescendantLeaves r = { v : Anderson4D.PlaneTree.Descendants r // ↑v ∈ t.Leaves }

@[reducible, inline]

abbrev Anderson4D.PlaneTree.DescendantBranches {t : PlaneTree} (r : t.VPos) : Type

Branch vertices of t below r, represented as descendant vertices.

Equations

• Anderson4D.PlaneTree.DescendantBranches r = { v : Anderson4D.PlaneTree.Descendants r // ↑v ∈ t.BranchNodes }

def Anderson4D.PlaneTree.subtreeLeafEquiv {t : PlaneTree} (r : t.VPos) : ↥(t.subtreeAt ↑r).Leaves ≃ DescendantLeaves r

Leaves of the rooted subtree are exactly descendant leaves.

Equations

• Anderson4D.PlaneTree.subtreeLeafEquiv r = (Anderson4D.PlaneTree.subtreeVertexEquiv r).subtypeEquiv ⋯

def Anderson4D.PlaneTree.subtreeBranchEquiv {t : PlaneTree} (r : t.VPos) : ↥(t.subtreeAt ↑r).BranchNodes ≃ DescendantBranches r

Branch vertices of the rooted subtree are exactly descendant branch vertices.

Equations

• Anderson4D.PlaneTree.subtreeBranchEquiv r = (Anderson4D.PlaneTree.subtreeVertexEquiv r).subtypeEquiv ⋯

def Anderson4D.PlaneTree.descendantLeavesEquivLeavesUnder {t : PlaneTree} (r : t.VPos) : DescendantLeaves r ≃ ↥(leavesUnder r)

Descendant leaves are the same carrier as membership in leavesUnder.

Equations

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

def Anderson4D.PlaneTree.subtreeLeafEquivLeavesUnder {t : PlaneTree} (r : t.VPos) : ↥(t.subtreeAt ↑r).Leaves ≃ ↥(leavesUnder r)

Paper-facing leaf equivalence: the leaves of the actual rooted subtree are precisely the original leaves in leavesUnder r.

Equations

• Anderson4D.PlaneTree.subtreeLeafEquivLeavesUnder r = (Anderson4D.PlaneTree.subtreeLeafEquiv r).trans (Anderson4D.PlaneTree.descendantLeavesEquivLeavesUnder r)

theorem Anderson4D.PlaneTree.card_leavesUnder_eq_leafCount_subtreeAt {t : PlaneTree} (r : t.VPos) : (leavesUnder r).card = (t.subtreeAt ↑r).leafCount

The recursive leaf count of the actual rooted subtree is the cardinality of the previously used prefix-defined leavesUnder finset.

Contracting a rooted subtree

def Anderson4D.PlaneTree.contractAt : PlaneTree → Pos → PlaneTree

Replace the rooted subtree at p by a single leaf. At an invalid step the tree is left unchanged; all structural theorems below assume IsPos t p.

Equations

• x✝.contractAt [] = Anderson4D.PlaneTree.leaf
• (Anderson4D.PlaneTree.node cs).contractAt (i :: p) = if h : i < cs.length then Anderson4D.PlaneTree.node (cs.set i (cs[i].contractAt p)) else Anderson4D.PlaneTree.node cs

def Anderson4D.PlaneTree.IsStrictDescendant (p q : Pos) : Prop

q lies strictly below p when it properly extends p.

Equations

• Anderson4D.PlaneTree.IsStrictDescendant p q = (p <+: q ∧ p ≠ q)

@[implicit_reducible]

instance Anderson4D.PlaneTree.instDecidablePredPosIsStrictDescendant (p : Pos) : DecidablePred (IsStrictDescendant p)

Equations

• Anderson4D.PlaneTree.instDecidablePredPosIsStrictDescendant p q = Anderson4D.PlaneTree.instDecidablePredPosIsStrictDescendant._aux_1 p q

@[simp]

theorem Anderson4D.PlaneTree.contractAt_nil (t : PlaneTree) : t.contractAt [] = leaf

theorem Anderson4D.PlaneTree.contractAt_cons_of_lt {cs : List PlaneTree} {i : ℕ} {p : Pos} (hi : i < cs.length) : (node cs).contractAt (i :: p) = node (cs.set i (cs[i].contractAt p))

theorem Anderson4D.PlaneTree.isPos_contractAt_iff {t : PlaneTree} {p q : Pos} (hp : t.IsPos p) : (t.contractAt p).IsPos q ↔ t.IsPos q ∧ ¬IsStrictDescendant p q

Contracting at p removes exactly the vertices strictly below p. The position p itself remains as the replacement leaf.

@[reducible, inline]

abbrev Anderson4D.PlaneTree.RetainedVertices (t : PlaneTree) (p : Pos) : Type

Vertices retained by contraction: all original vertices except those strictly below the contraction position.

Equations

• t.RetainedVertices p = { v : t.VPos // ¬Anderson4D.PlaneTree.IsStrictDescendant p ↑v }

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

Include a vertex of the contracted tree into the original tree. Its position path is unchanged.

Equations

• Anderson4D.PlaneTree.contractVertex hp v = ⟨↑v, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.contractVertex_val {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) : ↑(contractVertex hp v) = ↑v

def Anderson4D.PlaneTree.contractVertexEquiv {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).VPos ≃ t.RetainedVertices p

Vertices of the contracted tree are exactly the retained vertices of the original tree.

Equations

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

@[simp]

theorem Anderson4D.PlaneTree.contractVertexEquiv_apply_val {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) : ↑((contractVertexEquiv hp) v) = contractVertex hp v

theorem Anderson4D.PlaneTree.isValid_contractAt {t : PlaneTree} {p : Pos} (ht : t.isValid = true) (hp : t.IsPos p) : (t.contractAt p).isValid = true

Contracting a rooted subtree preserves Hepp validity.

theorem Anderson4D.PlaneTree.isPos_contractAt_self {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).IsPos p

The contraction position remains a valid position in the contracted tree.

def Anderson4D.PlaneTree.contractMarker (t : PlaneTree) (p : Pos) (hp : t.IsPos p) : (t.contractAt p).VPos

The vertex replacing the contracted subtree.

Equations

• t.contractMarker p hp = ⟨p, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.contractMarker_val (t : PlaneTree) (p : Pos) (hp : t.IsPos p) : ↑(t.contractMarker p hp) = p

theorem Anderson4D.PlaneTree.childCount_contractAt_self {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).childCount p = 0

The replacement vertex is a leaf.

theorem Anderson4D.PlaneTree.contractMarker_mem_Leaves (t : PlaneTree) (p : Pos) (hp : t.IsPos p) : t.contractMarker p hp ∈ (t.contractAt p).Leaves

theorem Anderson4D.PlaneTree.childCount_contractAt_eq_of_ne {t : PlaneTree} {p q : Pos} (hp : t.IsPos p) (hq : (t.contractAt p).IsPos q) (hne : q ≠ p) : (t.contractAt p).childCount q = t.childCount q

Away from the replacement vertex, contraction preserves child counts at every retained vertex.

@[reducible, inline]

abbrev Anderson4D.PlaneTree.BranchesOutside (t : PlaneTree) (p : Pos) : Type

Original branch vertices surviving contraction. The root of the removed subtree is excluded because it becomes the marker leaf.

Equations

• t.BranchesOutside p = { v : ↥t.BranchNodes // ¬p <+: ↑↑v }

@[reducible, inline]

abbrev Anderson4D.PlaneTree.LeavesOutside (t : PlaneTree) (p : Pos) : Type

Original leaves outside the contracted rooted subtree.

Equations

• t.LeavesOutside p = { v : ↥t.Leaves // ¬p <+: ↑↑v }

theorem Anderson4D.PlaneTree.mem_BranchNodes_contractVertex_iff_of_ne {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) (hne : ↑v ≠ p) : v ∈ (t.contractAt p).BranchNodes ↔ contractVertex hp v ∈ t.BranchNodes

theorem Anderson4D.PlaneTree.mem_Leaves_contractVertex_iff_of_ne {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) (hne : ↑v ≠ p) : v ∈ (t.contractAt p).Leaves ↔ contractVertex hp v ∈ t.Leaves

theorem Anderson4D.PlaneTree.not_prefix_of_mem_BranchNodes_contractAt {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) (hv : v ∈ (t.contractAt p).BranchNodes) : ¬p <+: ↑v

A branch vertex of the contracted tree cannot lie weakly below the contraction position: the only retained vertex there is the marker leaf.

theorem Anderson4D.PlaneTree.not_prefix_of_ne_contractAt {t : PlaneTree} {p : Pos} (hp : t.IsPos p) (v : (t.contractAt p).VPos) (hne : ↑v ≠ p) : ¬p <+: ↑v

A retained vertex distinct from the marker lies completely outside the contracted rooted subtree.

def Anderson4D.PlaneTree.contractBranchEquiv {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : ↥(t.contractAt p).BranchNodes ≃ t.BranchesOutside p

Branch vertices of the contracted tree are exactly the original branch vertices outside the removed rooted subtree.

Equations

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

theorem Anderson4D.PlaneTree.card_BranchNodes_contractAt_eq_card_branchesOutside {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).BranchNodes.card = Fintype.card (t.BranchesOutside p)

Cardinal form of contractBranchEquiv.

def Anderson4D.PlaneTree.contractLeafEquiv {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : ↥(t.contractAt p).Leaves ≃ Option (t.LeavesOutside p)

Leaves of the contracted tree consist of the new marker leaf together with the original leaves outside the removed rooted subtree. none denotes the marker and some l denotes an unchanged outside leaf.

Equations

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

theorem Anderson4D.PlaneTree.card_Leaves_contractAt_eq_card_option_leavesOutside {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).Leaves.card = Fintype.card (Option (t.LeavesOutside p))

Cardinal form of contractLeafEquiv.

theorem Anderson4D.PlaneTree.subtreeAt_contractAt_self {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).subtreeAt p = leaf

Looking below the replacement vertex gives the bare leaf.

theorem Anderson4D.PlaneTree.contractAt_size_add_subtreeAt_size {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).size + (t.subtreeAt p).size = t.size + 1

Exact vertex-count ledger for contraction: the contracted tree and the removed subtree overlap in precisely their common replacement/root vertex.

theorem Anderson4D.PlaneTree.contractAt_leafCount_add_subtreeAt_leafCount {t : PlaneTree} {p : Pos} (hp : t.IsPos p) : (t.contractAt p).leafCount + (t.subtreeAt p).leafCount = t.leafCount + 1

Exact leaf-count ledger for contraction. The marker replaces all leaves of the removed subtree, hence the correction term + 1.

theorem Anderson4D.PlaneTree.one_lt_subtreeAt_size_of_branch {t : PlaneTree} {r : t.VPos} (hr : r ∈ t.BranchNodes) : 1 < (t.subtreeAt ↑r).size

A subtree rooted at a branch vertex has more than one vertex.

theorem Anderson4D.PlaneTree.contractAt_size_lt_of_branch {t : PlaneTree} {r : t.VPos} (hr : r ∈ t.BranchNodes) : (t.contractAt ↑r).size < t.size

Contracting at a branch vertex strictly decreases tree size.