Data transport for the subtree-collapse induction

This file transports markings, multiplicities, and leaf carriers through the two tree operations used in paper §5.4.1:

• restriction to the rooted subtree at r;
• contraction of that subtree to the marker leaf at r.

The constructions preserve all meaningful values definitionally. The theorems below expose the resulting scale and multiplicity ledgers without depending on the later word, geometry, or summation layers.

Parent transport

theorem Anderson4D.parentV_subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) (hv : v ≠ (t.subtreeAt ↑r).rootV) : PlaneTree.parentV (PlaneTree.subtreeVertex r v) = PlaneTree.subtreeVertex r (PlaneTree.parentV v)

Prepending a fixed subtree root commutes with the parent map away from the root of the smaller tree.

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

The unchanged paths in a contracted tree make its vertex inclusion commute with the parent map.

Markings

def Anderson4D.restrictMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) : (t.subtreeAt ↑r).HeppMarking

Restrict a Hepp marking to the actual rooted subtree at r.

Equations

• Anderson4D.restrictMarking Nm r = { Nexp := fun (v : (t.subtreeAt ↑r).VPos) => Nm.Nexp (Anderson4D.PlaneTree.subtreeVertex r v), pos := ⋯, parent_gt := ⋯ }

@[simp]

theorem Anderson4D.scaleN_restrictMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : scaleN (restrictMarking Nm r) v = scaleN Nm (PlaneTree.subtreeVertex r v)

Restricting a marking preserves every subtree scale exactly.

def Anderson4D.contractMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) : (t.contractAt ↑r).HeppMarking

Contract a Hepp marking by retaining the exponent of every surviving branch. The marker is a leaf, so its stored exponent is irrelevant.

Equations

• Anderson4D.contractMarking Nm r = { Nexp := fun (v : (t.contractAt ↑r).VPos) => Nm.Nexp (Anderson4D.PlaneTree.contractVertex ⋯ v), pos := ⋯, parent_gt := ⋯ }

@[simp]

theorem Anderson4D.scaleN_contractMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (v : (t.contractAt ↑r).VPos) : scaleN (contractMarking Nm r) v = scaleN Nm (PlaneTree.contractVertex ⋯ v)

Contracting a marking preserves every surviving branch scale exactly.

Inside and outside leaf carriers

@[reducible, inline]

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

Original leaves weakly below the selected subtree root.

Equations

• Anderson4D.InsideLeaf r = { l : Anderson4D.HeppLeaf t // ↑r <+: ↑↑l }

@[reducible, inline]

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

Original leaves outside the selected rooted subtree.

Equations

• Anderson4D.OutsideLeaf r = { l : Anderson4D.HeppLeaf t // ¬↑r <+: ↑↑l }

def Anderson4D.leafInsideOutsideEquiv {t : PlaneTree} (r : t.VPos) : HeppLeaf t ≃ InsideLeaf r ⊕ OutsideLeaf r

Every original leaf is uniquely either inside or outside the selected rooted subtree.

Equations

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

def Anderson4D.restrictLeafEquiv {t : PlaneTree} (r : t.VPos) : HeppLeaf (t.subtreeAt ↑r) ≃ InsideLeaf r

The leaves of the rooted subtree are exactly the original inside leaves.

Equations

• Anderson4D.restrictLeafEquiv r = (Anderson4D.PlaneTree.subtreeLeafEquivLeavesUnder r).trans ((Equiv.refl (Anderson4D.HeppLeaf t)).subtypeEquiv ⋯)

def Anderson4D.contractMarkerLeaf {t : PlaneTree} (r : t.VPos) : HeppLeaf (t.contractAt ↑r)

The distinguished marker leaf in the contracted tree.

Equations

• Anderson4D.contractMarkerLeaf r = ⟨t.contractMarker ↑r ⋯, ⋯⟩

def Anderson4D.contractLeafSumEquiv {t : PlaneTree} (r : t.VPos) : HeppLeaf (t.contractAt ↑r) ≃ Unit ⊕ OutsideLeaf r

Contracted leaves are the marker together with all unchanged outside leaves.

Equations

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

@[simp]

theorem Anderson4D.contractLeafSumEquiv_marker {t : PlaneTree} (r : t.VPos) : (contractLeafSumEquiv r) (contractMarkerLeaf r) = Sum.inl ()

Canonical leaves, compound sets, and embeddings

def Anderson4D.restrictInsideLeaf {t : PlaneTree} (r : t.VPos) (l : InsideLeaf r) : HeppLeaf (t.subtreeAt ↑r)

View a chosen original inside leaf as a leaf of the restricted subtree.

Equations

• Anderson4D.restrictInsideLeaf r l = (Anderson4D.restrictLeafEquiv r).symm l

@[simp]

theorem Anderson4D.subtreeVertex_restrictInsideLeaf {t : PlaneTree} (r : t.VPos) (l : InsideLeaf r) : PlaneTree.subtreeVertex r ↑(restrictInsideLeaf r l) = ↑↑l

def Anderson4D.contractOutsideLeaf {t : PlaneTree} (r : t.VPos) (l : OutsideLeaf r) : HeppLeaf (t.contractAt ↑r)

View an original outside leaf as the corresponding unchanged leaf of the contracted tree.

Equations

• Anderson4D.contractOutsideLeaf r l = (Anderson4D.contractLeafSumEquiv r).symm (Sum.inr l)

@[simp]

theorem Anderson4D.contractLeafSumEquiv_contractOutsideLeaf {t : PlaneTree} (r : t.VPos) (l : OutsideLeaf r) : (contractLeafSumEquiv r) (contractOutsideLeaf r l) = Sum.inr l

@[simp]

theorem Anderson4D.contractVertex_contractOutsideLeaf {t : PlaneTree} (r : t.VPos) (l : OutsideLeaf r) : PlaneTree.contractVertex ⋯ ↑(contractOutsideLeaf r l) = ↑↑l

def Anderson4D.restrictCompound {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) : Finset (t.subtreeAt ↑r).VPos

Restrict a vertex set to the selected subtree. Applied to the paper's compound-leaf set, only its inside leaves survive.

Equations

• Anderson4D.restrictCompound r compound = {v : (t.subtreeAt ↑r).VPos | Anderson4D.PlaneTree.subtreeVertex r v ∈ compound}

@[simp]

theorem Anderson4D.mem_restrictCompound {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (v : (t.subtreeAt ↑r).VPos) : v ∈ restrictCompound r compound ↔ PlaneTree.subtreeVertex r v ∈ compound

def Anderson4D.contractCompound {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) : Finset (t.contractAt ↑r).VPos

Contract a compound-leaf set. The marker is declared compound, and an unchanged outside vertex is compound exactly when its original vertex was.

Equations

• Anderson4D.contractCompound r compound = {v : (t.contractAt ↑r).VPos | ↑v = ↑r ∨ Anderson4D.PlaneTree.contractVertex ⋯ v ∈ compound}

@[simp]

theorem Anderson4D.mem_contractCompound {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (v : (t.contractAt ↑r).VPos) : v ∈ contractCompound r compound ↔ ↑v = ↑r ∨ PlaneTree.contractVertex ⋯ v ∈ compound

@[simp]

theorem Anderson4D.contractMarker_mem_contractCompound {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) : t.contractMarker ↑r ⋯ ∈ contractCompound r compound

@[simp]

theorem Anderson4D.restrictInsideLeaf_mem_restrictCompound_iff {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (l : InsideLeaf r) : ↑(restrictInsideLeaf r l) ∈ restrictCompound r compound ↔ ↑↑l ∈ compound

@[simp]

theorem Anderson4D.contractOutsideLeaf_mem_contractCompound_iff {t : PlaneTree} (r : t.VPos) (compound : Finset t.VPos) (l : OutsideLeaf r) : ↑(contractOutsideLeaf r l) ∈ contractCompound r compound ↔ ↑↑l ∈ compound

def Anderson4D.restrictEmbedding {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) : HeppLeaf (t.subtreeAt ↑r) → Fin 4 → ℤ

Restriction of an embedding to the actual subtree leaf carrier.

Equations

• Anderson4D.restrictEmbedding z r l = z ↑((Anderson4D.restrictLeafEquiv r) l)

@[simp]

theorem Anderson4D.restrictEmbedding_apply_inside {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (l : InsideLeaf r) : restrictEmbedding z r (restrictInsideLeaf r l) = z ↑l

def Anderson4D.contractEmbedding {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) : HeppLeaf (t.contractAt ↑r) → Fin 4 → ℤ

Contract an embedding by placing the marker at a specified original inside leaf lstar and retaining all outside leaf positions.

Equations

• Anderson4D.contractEmbedding z r lstar l = Sum.elim (fun (x : Unit) => z ↑lstar) (fun (lout : Anderson4D.OutsideLeaf r) => z ↑lout) ((Anderson4D.contractLeafSumEquiv r) l)

@[simp]

theorem Anderson4D.contractEmbedding_apply_marker {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) : contractEmbedding z r lstar (contractMarkerLeaf r) = z ↑lstar

@[simp]

theorem Anderson4D.contractEmbedding_apply_outside {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (l : OutsideLeaf r) : contractEmbedding z r lstar (contractOutsideLeaf r l) = z ↑l

theorem Anderson4D.restrictCompound_subset_leaves {t : PlaneTree} (r : t.VPos) {compound : Finset t.VPos} (hc : compound ⊆ t.Leaves) : restrictCompound r compound ⊆ (t.subtreeAt ↑r).Leaves

theorem Anderson4D.contractCompound_subset_leaves {t : PlaneTree} (r : t.VPos) {compound : Finset t.VPos} (hc : compound ⊆ t.Leaves) : contractCompound r compound ⊆ (t.contractAt ↑r).Leaves

Multiplicities

def Anderson4D.restrictMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : (t.subtreeAt ↑r).Multiplicities

Restrict leaf multiplicities to the selected rooted subtree.

Equations

• Anderson4D.restrictMultiplicities mu r = { m := fun (v : (t.subtreeAt ↑r).VPos) => mu.m (Anderson4D.PlaneTree.subtreeVertex r v), two_le := ⋯ }

@[simp]

theorem Anderson4D.restrictMultiplicities_m {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : (restrictMultiplicities mu r).m v = mu.m (PlaneTree.subtreeVertex r v)

@[simp]

theorem Anderson4D.restrictMultiplicities_inside {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (l : InsideLeaf r) : leafMultiplicity (restrictMultiplicities mu r) (restrictInsideLeaf r l) = leafMultiplicity mu ↑l

def Anderson4D.contractMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : (t.contractAt ↑r).Multiplicities

Contract leaf multiplicities. The new marker has multiplicity s+1; all unchanged outside leaves inherit their original multiplicity.

Equations

• Anderson4D.contractMultiplicities mu r s hs = { m := fun (v : (t.contractAt ↑r).VPos) => if ↑v = ↑r then s + 1 else mu.m (Anderson4D.PlaneTree.contractVertex ⋯ v), two_le := ⋯ }

@[simp]

theorem Anderson4D.contractMultiplicities_marker {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : leafMultiplicity (contractMultiplicities mu r s hs) (contractMarkerLeaf r) = s + 1

theorem Anderson4D.contractMultiplicities_m_of_ne {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) : (contractMultiplicities mu r s hs).m v = mu.m (PlaneTree.contractVertex ⋯ v)

@[simp]

theorem Anderson4D.contractMultiplicities_outside {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (l : OutsideLeaf r) : leafMultiplicity (contractMultiplicities mu r s hs) (contractOutsideLeaf r l) = leafMultiplicity mu ↑l

def Anderson4D.insideMultiplicityTotal {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : ℕ

Total multiplicity carried by the leaves inside the selected subtree.

Equations

• Anderson4D.insideMultiplicityTotal mu r = ∑ l : Anderson4D.InsideLeaf r, Anderson4D.leafMultiplicity mu ↑l

def Anderson4D.outsideMultiplicityTotal {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : ℕ

Total multiplicity carried by the leaves outside the selected subtree.

Equations

• Anderson4D.outsideMultiplicityTotal mu r = ∑ l : Anderson4D.OutsideLeaf r, Anderson4D.leafMultiplicity mu ↑l

theorem Anderson4D.totalMultiplicity_restrictMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : totalMultiplicity (restrictMultiplicities mu r) = insideMultiplicityTotal mu r

Restriction preserves exactly the total multiplicity of the inside leaves.

theorem Anderson4D.totalMultiplicity_eq_inside_add_outside {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : totalMultiplicity mu = insideMultiplicityTotal mu r + outsideMultiplicityTotal mu r

The original total multiplicity splits exactly into inside and outside parts.

theorem Anderson4D.totalMultiplicity_contractMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : totalMultiplicity (contractMultiplicities mu r s hs) = s + 1 + outsideMultiplicityTotal mu r

Under contraction, the total multiplicity is the marker contribution s+1 plus the unchanged outside contribution.

theorem Anderson4D.totalMultiplicity_contract_add_restrict {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : totalMultiplicity (contractMultiplicities mu r s hs) + totalMultiplicity (restrictMultiplicities mu r) = totalMultiplicity mu + (s + 1)

Exact total ledger: the contracted and restricted problems together contain the original mass plus the new marker mass.