Fixed-word connector for the collapse induction

This module transports the two word predicates and the chain products from raw collapse coordinates to the actual restricted and contracted Hepp-tree alphabets. It is the pointwise connector between the raw summand and the two subproblems in paper (5.43).

Predicate transport through alphabet renaming

theorem Anderson4D.noAdjacentOutside_wordRename_iff {α : Type u_1} {β : Type u_2} {m : ℕ} [DecidableEq α] [DecidableEq β] (e : α ≃ β) (O : Finset (AdjacentIndex m)) (w : Fin m → α) : NoAdjacentOutside O ((wordRenameEquiv e m) w) ↔ NoAdjacentOutside O w

NoAdjacentOutside is invariant under an alphabet equivalence.

theorem Anderson4D.RawCollapseData.restrictedInsideWord_noAdjacentOutside {t : PlaneTree} {r : t.VPos} (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hadjacent : NoAdjacentEqual d.expandedWord) : NoAdjacentOutside d.adjacentCutIndices (restrictedInsideWord r d)

The original finite-word adjacency condition supplies the exact restricted-tree predicate required by Proposition 5.10.

theorem Anderson4D.RawCollapseData.contractedCollapsedWord_noAdjacentEqual {t : PlaneTree} {r : t.VPos} (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hadjacent : NoAdjacentEqual d.expandedWord) : NoAdjacentEqual (contractedCollapsedWord r d)

The collapsed word on the actual contracted-tree alphabet inherits unequal neighbours.

theorem Anderson4D.RawCollapseData.contractedCollapsedWord_noProperLeafBlock {t : PlaneTree} {r : t.VPos} (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hprimitive : NoProperLeafBlock d.expandedWord) : NoProperLeafBlock (contractedCollapsedWord r d)

The collapsed word on the actual contracted-tree alphabet inherits the paper's proper-leaf-block condition.

theorem Anderson4D.RawCollapseData.contractedCollapsedWord_primitiveSeparated {t : PlaneTree} {r : t.VPos} (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hprimitive : NoProperLeafBlock d.expandedWord) (hadjacent : NoAdjacentEqual d.expandedWord) : NoProperLeafBlock (contractedCollapsedWord r d) ∧ NoAdjacentEqual (contractedCollapsedWord r d)

Both predicates required by the contracted primitive-separated subproblem.

Collapsed-chain exact connector

theorem Anderson4D.collapsedCollapsePoint_contractCollapsedAlphabetEquiv_symm {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) : (fun (l : HeppLeaf (t.contractAt ↑r)) => collapsedCollapsePoint z r lstar ((contractCollapsedAlphabetEquiv r).symm l)) = contractEmbedding z r lstar

Pulling the contracted embedding back to the raw marker/outside alphabet is exactly collapsedCollapsePoint.

theorem Anderson4D.RawCollapseData.collapsedChainProduct_eq_heppChainWeight {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : listChainProduct (collapsedCollapseEdge z r lstar) d.collapsed = heppChainWeight (contractEmbedding z r lstar) (contractedCollapsedWord r d)

The raw collapsed list chain is exactly the chain weight of the renamed word on the actual contracted tree.

theorem Anderson4D.RawCollapseData.collapsedChainProduct_eq_primitiveSeparatedChainWeight {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hprimitive : NoProperLeafBlock d.expandedWord) (hadjacent : NoAdjacentEqual d.expandedWord) : listChainProduct (collapsedCollapseEdge z r lstar) d.collapsed = primitiveSeparatedChainWeight (contractEmbedding z r lstar) (contractedCollapsedWord r d)

Under the transported predicates, the raw collapsed chain is the actual contracted primitive-separated summand.

Active raw summand

theorem Anderson4D.splitLeafPosition_eq_originalCollapsePoint {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) : splitLeafPosition r z = originalCollapsePoint z

The split-alphabet position from the exact reindexing is the position used by the geometric collapse estimate.

theorem Anderson4D.RawCollapseData.rawPrimitiveSeparatedChainWeight_eq_originalChain {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) {r : t.VPos} (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hprimitive : NoProperLeafBlock d.expandedWord) (hadjacent : NoAdjacentEqual d.expandedWord) : rawPrimitiveSeparatedChainWeight (splitLeafPosition r z) d = listChainProduct (originalCollapseEdge z) d.expandWord

On an active raw datum, the raw statistic is exactly the original split-alphabet list chain used by the geometric (5.43) estimate.

Fixed-word (5.43)

theorem Anderson4D.RawCollapseData.rawPrimitiveSeparatedChainWeight_le_fixedWordFactors {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)) (hprimitive : NoProperLeafBlock d.expandedWord) (hadjacent : NoAdjacentEqual d.expandedWord) : rawPrimitiveSeparatedChainWeight (splitLeafPosition r z) d ≤ 4 ^ d.insideLength * singleScaleChainWeight (restrictEmbedding z r) d.adjacentCutIndices (restrictedInsideWord r d) * primitiveSeparatedChainWeight (contractEmbedding z r lstar) (contractedCollapsedWord r d)

Pointwise connector from an active raw primitive-separated summand to the actual restricted single-scale and contracted primitive-separated subproblems.