Tree-geometric boundary comparison for the collapse chain

This file connects the raw segmented-chain estimate of CollapseChain to the actual inside/outside leaf carriers and lattice edge weights used in paper (5.43).

Tree-facing edge functions

def Anderson4D.originalCollapsePoint {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} : InsideLeaf r ⊕ OutsideLeaf r → Fin 4 → ℤ

Position of an original split letter.

Equations

• Anderson4D.originalCollapsePoint z (Sum.inl l) = z ↑l
• Anderson4D.originalCollapsePoint z (Sum.inr y) = z ↑y

def Anderson4D.collapsedCollapsePoint {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) : Unit ⊕ OutsideLeaf r → Fin 4 → ℤ

Position of a collapsed letter: the marker is represented by lstar, and outside leaves keep their original positions.

Equations

• Anderson4D.collapsedCollapsePoint z r lstar (Sum.inl val) = Anderson4D.contractEmbedding z r lstar (Anderson4D.contractMarkerLeaf r)
• Anderson4D.collapsedCollapsePoint z r lstar (Sum.inr y) = Anderson4D.contractEmbedding z r lstar (Anderson4D.contractOutsideLeaf r y)

noncomputable def Anderson4D.originalCollapseEdge {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} (x y : InsideLeaf r ⊕ OutsideLeaf r) : ℝ

Original lattice edge on the inside/outside split alphabet.

Equations

• Anderson4D.originalCollapseEdge z x y = Anderson4D.latticeEdgeWeight (Anderson4D.originalCollapsePoint z x) (Anderson4D.originalCollapsePoint z y)

noncomputable def Anderson4D.collapsedCollapseEdge {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (x y : Unit ⊕ OutsideLeaf r) : ℝ

Collapsed lattice edge on the marker/outside alphabet.

Equations

• Anderson4D.collapsedCollapseEdge z r lstar x y = Anderson4D.latticeEdgeWeight (Anderson4D.collapsedCollapsePoint z r lstar x) (Anderson4D.collapsedCollapsePoint z r lstar y)

theorem Anderson4D.originalCollapseEdge_nonneg {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} (x y : InsideLeaf r ⊕ OutsideLeaf r) : 0 ≤ originalCollapseEdge z x y

theorem Anderson4D.collapsedCollapseEdge_nonneg {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (x y : Unit ⊕ OutsideLeaf r) : 0 ≤ collapsedCollapseEdge z r lstar x y

Structural shape of canonical collapse segments

def Anderson4D.IsCanonicalCollapseSegment {A : Type u_1} {B : Type u_2} (p : ChainSegment (A ⊕ B) (Unit ⊕ B)) : Prop

Every canonical collapse segment is either an outside singleton or a nonempty block consisting entirely of inside letters.

Equations

• Anderson4D.IsCanonicalCollapseSegment p = ((∃ (b : B), p.tag = Sum.inr b ∧ p.letters = [Sum.inr b]) ∨ ∃ (block : List A), block ≠ [] ∧ p.tag = Sum.inl () ∧ p.letters = List.map Sum.inl block)

theorem Anderson4D.canonical_of_mem_collapseSegmentsAux {A : Type u_1} {B : Type u_2} (blocks : List (List A)) (collapsed : List (Unit ⊕ B)) (hblocks : ∀ block ∈ blocks, block ≠ []) (p : ChainSegment (A ⊕ B) (Unit ⊕ B)) : p ∈ collapseSegmentsAux blocks collapsed hblocks → IsCanonicalCollapseSegment p

theorem Anderson4D.RawCollapseData.canonical_chainSegment {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (p : ChainSegment (A ⊕ B) (Unit ⊕ B)) (hp : p ∈ d.chainSegments) : IsCanonicalCollapseSegment p

Local changed-boundary comparison

theorem Anderson4D.canonical_segmentBoundary_le {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (p q : ChainSegment (InsideLeaf r ⊕ OutsideLeaf r) (Unit ⊕ OutsideLeaf r)) (hp : IsCanonicalCollapseSegment p) (hq : IsCanonicalCollapseSegment q) (htags : p.tag.isLeft = false ∨ q.tag.isLeft = false) : segmentBoundaryEdge (originalCollapseEdge z) p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedCollapseEdge z r lstar p.tag q.tag

The geometric comparison for a single adjacent pair of canonical segments. The impossible marker-marker case is ruled out by the tag-chain hypothesis inherited from NoTwoAdjacentMarkers.

theorem Anderson4D.RawCollapseData.chainSegments_isChain_boundaryComparison {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : List.IsChain (fun (p q : ChainSegment (InsideLeaf r ⊕ OutsideLeaf r) (Unit ⊕ OutsideLeaf r)) => segmentBoundaryEdge (originalCollapseEdge z) p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedCollapseEdge z r lstar p.tag q.tag) d.chainSegments

Canonical segments of raw collapse data satisfy the local comparison required by the raw chain theorem.

Tree-facing (5.43)

theorem Anderson4D.RawCollapseData.expandWord_latticeChain_le_four_pow {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : listChainProduct (originalCollapseEdge z) d.expandWord ≤ 4 ^ d.insideLength * insideBlockChainProduct (originalCollapseEdge z) d * listChainProduct (collapsedCollapseEdge z r lstar) d.collapsed

Tree-geometric form of paper (5.43): the expanded original chain is bounded by the internal inside-block chains times the collapsed chain, with the corrected loss 4^(total inside length).

Coordinate-product identity

The geometric (5.43) estimate combines with the exact identity

d.insideBlockChainProduct (originalCollapseEdge z) = heppChainWeightExcept (restrictEmbedding z r) d.adjacentCutIndices (restrictedInsideWord r d).

This is the finite-product reindexing statement that deleting the blockComposition proper partial-sum gaps from the flattened inside word leaves exactly the product of the internal block chains; it is independent of the boundary geometry proved here.