Tree-facing collapse coordinates

This module connects the pure (π₁, O, π₂) collapse coordinates to the actual leaf alphabets of the restricted and contracted Hepp trees.

Named alphabet and word equivalences

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

Rename inside letters as leaves of the actual restricted subtree.

Equations

• Anderson4D.restrictInsideAlphabetEquiv r = (Anderson4D.restrictLeafEquiv r).symm

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

Rename the marker/outside alphabet as leaves of the contracted tree.

Equations

• Anderson4D.contractCollapsedAlphabetEquiv r = (Anderson4D.contractLeafSumEquiv r).symm

def Anderson4D.restrictInsideWordEquiv {t : PlaneTree} (r : t.VPos) (n : ℕ) : (Fin n → InsideLeaf r) ≃ (Fin n → HeppLeaf (t.subtreeAt ↑r))

Word equivalence used for the Proposition 5.10 call on the subtree.

Equations

• Anderson4D.restrictInsideWordEquiv r n = Anderson4D.wordRenameEquiv (Anderson4D.restrictInsideAlphabetEquiv r) n

def Anderson4D.contractCollapsedWordEquiv {t : PlaneTree} (r : t.VPos) (n : ℕ) : (Fin n → Unit ⊕ OutsideLeaf r) ≃ (Fin n → HeppLeaf (t.contractAt ↑r))

Word equivalence used for the induction call on the contracted tree.

Equations

• Anderson4D.contractCollapsedWordEquiv r n = Anderson4D.wordRenameEquiv (Anderson4D.contractCollapsedAlphabetEquiv r) n

Multiplicity identities

def Anderson4D.restrictedCoordinateMultiplicity {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : HeppLeaf (t.subtreeAt ↑r) → ℕ

Inside coordinate multiplicity transported to the restricted tree.

Equations

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

theorem Anderson4D.restrictedCoordinateMultiplicity_eq {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : restrictedCoordinateMultiplicity mu r = leafMultiplicity (restrictMultiplicities mu r)

The transported inside multiplicity is exactly the restricted tree's leaf multiplicity.

def Anderson4D.collapseCutCount {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : ℕ

The paper cut count s, read from the number s+1 of inside blocks.

Equations

• Anderson4D.collapseCutCount d = d.blocks.length - 1

theorem Anderson4D.collapseCutCount_add_one {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (hblocks : 2 ≤ d.blocks.length) : collapseCutCount d + 1 = d.blocks.length

theorem Anderson4D.one_le_collapseCutCount {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (hblocks : 2 ≤ d.blocks.length) : 1 ≤ collapseCutCount d

def Anderson4D.contractedCoordinateMultiplicity {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : HeppLeaf (t.contractAt ↑r) → ℕ

Collapsed coordinate multiplicity transported to the contracted tree.

Equations

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

theorem Anderson4D.collapsedMultiplicity_marker_eq_contract {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hblocks : 2 ≤ d.blocks.length) : collapsedMultiplicity (splitLeafMultiplicity mu r) d (Sum.inl ()) = leafMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯) (contractMarkerLeaf r)

Marker branch of the contracted multiplicity identity.

theorem Anderson4D.collapsedMultiplicity_outside_eq_contract {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hblocks : 2 ≤ d.blocks.length) (l : OutsideLeaf r) : collapsedMultiplicity (splitLeafMultiplicity mu r) d (Sum.inr l) = leafMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯) (contractOutsideLeaf r l)

Outside branch of the contracted multiplicity identity.

theorem Anderson4D.contractedCoordinateMultiplicity_eq {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hblocks : 2 ≤ d.blocks.length) : contractedCoordinateMultiplicity mu r d = leafMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯)

The transported collapsed multiplicity is exactly the contracted tree's leaf multiplicity, including the new marker multiplicity s+1.

Coordinate words on the actual tree alphabets

def Anderson4D.restrictedInsideWord {t : PlaneTree} (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : Fin d.insideLength → HeppLeaf (t.subtreeAt ↑r)

The inside coordinate word, renamed as a word of restricted-tree leaves.

Equations

• Anderson4D.restrictedInsideWord r d = (Anderson4D.restrictInsideWordEquiv r d.insideLength) d.insideWord

def Anderson4D.contractedCollapsedWord {t : PlaneTree} (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : Fin d.collapsed.length → HeppLeaf (t.contractAt ↑r)

The collapsed coordinate word, renamed as a word of contracted-tree leaves.

Equations

• Anderson4D.contractedCollapsedWord r d = (Anderson4D.contractCollapsedWordEquiv r d.collapsed.length) d.collapsedWord

@[simp]

theorem Anderson4D.restrictedInsideWord_apply {t : PlaneTree} (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (i : Fin d.insideLength) : restrictedInsideWord r d i = (restrictLeafEquiv r).symm (d.insideWord i)

@[simp]

theorem Anderson4D.contractedCollapsedWord_apply {t : PlaneTree} (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (i : Fin d.collapsed.length) : contractedCollapsedWord r d i = (contractLeafSumEquiv r).symm (d.collapsedWord i)

theorem Anderson4D.restrictedInsideWord_mem_validWords {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) : restrictedInsideWord r d ∈ validWords (leafMultiplicity (restrictMultiplicities mu r))

Multiplicity specification on raw coordinates gives a valid word on the actual restricted-tree leaf alphabet.

theorem Anderson4D.contractedCollapsedWord_mem_validWords {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) : contractedCollapsedWord r d ∈ validWords (leafMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯))

Multiplicity specification on raw coordinates gives a valid word on the actual contracted-tree leaf alphabet.

Length and total-multiplicity interfaces

theorem Anderson4D.sum_multiplicity_eq_wordLength {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {mult : α → ℕ} {w : Fin n → α} (hw : w ∈ validWords mult) : ∑ a : α, mult a = n

A valid word's prescribed multiplicities sum to its word length.

theorem Anderson4D.totalMultiplicity_restrict_eq_insideLength {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) : totalMultiplicity (restrictMultiplicities mu r) = d.insideLength

The inside coordinate length is exactly the total multiplicity of the restricted tree.

theorem Anderson4D.totalMultiplicity_contract_eq_collapsedLength {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) : totalMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯) = d.collapsed.length

The collapsed coordinate length is exactly the total multiplicity of the contracted tree.

theorem Anderson4D.totalMultiplicity_contract_eq_lengthLedger {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hblocks : 2 ≤ d.blocks.length) : totalMultiplicity (contractMultiplicities mu r (collapseCutCount d) ⋯) = d.expandedLength - d.insideLength + d.blocks.length

Original-length form of the contracted total-multiplicity ledger.