Inside-block chains and the cut-exception chain

This file proves the exact connector used in the collapse step: multiplying the consecutive weights internal to the maximal inside blocks is the same as multiplying the flattened inside-word chain after omitting precisely the proper composition cuts.

@[reducible, inline]

abbrev Anderson4D.RawCollapseData.InsideBlockGap {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Type

A gap internal to one block of the inside-word composition.

Equations

• d.InsideBlockGap = ((i : Fin d.blockComposition.length) × Fin (d.blockComposition.blocksFun i - 1))

def Anderson4D.RawCollapseData.insideBlockWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (i : Fin d.blockComposition.length) : Fin (d.blockComposition.blocksFun i) → A

The ith composition block, read directly from the flattened inside word.

Equations

• d.insideBlockWord i j = d.insideWord ((d.blockComposition.embedding i) j)

theorem Anderson4D.RawCollapseData.ofFn_insideBlockWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (i : Fin d.blockComposition.length) : List.ofFn (d.insideBlockWord i) = d.blocks.get ⟨↑i, ⋯⟩

The composition view of a block recovers the recorded list block.

def Anderson4D.RawCollapseData.insideBlockGapLeft {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : Fin d.insideLength

The left endpoint in the flattened inside word of an internal block gap.

Equations

• d.insideBlockGapLeft g = (d.blockComposition.embedding g.fst) ⟨↑g.snd, ⋯⟩

def Anderson4D.RawCollapseData.insideBlockGapRight {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : Fin d.insideLength

The right endpoint in the flattened inside word of an internal block gap.

Equations

• d.insideBlockGapRight g = (d.blockComposition.embedding g.fst) ⟨↑g.snd + 1, ⋯⟩

@[simp]

theorem Anderson4D.RawCollapseData.insideBlockGapLeft_val {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : ↑(d.insideBlockGapLeft g) = d.blockComposition.sizeUpTo ↑g.fst + ↑g.snd

@[simp]

theorem Anderson4D.RawCollapseData.insideBlockGapRight_val {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : ↑(d.insideBlockGapRight g) = d.blockComposition.sizeUpTo ↑g.fst + ↑g.snd + 1

def Anderson4D.RawCollapseData.insideBlockGapAdjacentIndex {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : AdjacentIndex d.insideLength

An internal block gap, regarded as an adjacency index of the flattened inside word.

Equations

• d.insideBlockGapAdjacentIndex g = ⟨d.insideBlockGapLeft g, ⋯⟩

@[simp]

theorem Anderson4D.RawCollapseData.insideBlockGapAdjacentIndex_val {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : ↑↑(d.insideBlockGapAdjacentIndex g) = d.blockComposition.sizeUpTo ↑g.fst + ↑g.snd

@[simp]

theorem Anderson4D.RawCollapseData.adjacentSucc_insideBlockGapAdjacentIndex {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : adjacentSucc (d.insideBlockGapAdjacentIndex g) = d.insideBlockGapRight g

theorem Anderson4D.RawCollapseData.insideBlockGapAdjacentIndex_injective {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Function.Injective d.insideBlockGapAdjacentIndex

def Anderson4D.RawCollapseData.insideBlockGapEmbedding {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.InsideBlockGap ↪ AdjacentIndex d.insideLength

The canonical embedding of internal block gaps into flattened adjacency indices.

Equations

• d.insideBlockGapEmbedding = { toFun := d.insideBlockGapAdjacentIndex, inj' := ⋯ }

theorem Anderson4D.RawCollapseData.insideBlockGapAdjacentIndex_not_mem {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (g : d.InsideBlockGap) : d.insideBlockGapAdjacentIndex g ∉ d.adjacentCutIndices

An internal block gap is never a proper composition cut.

theorem Anderson4D.RawCollapseData.exists_insideBlockGap_of_not_mem {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (edge : AdjacentIndex d.insideLength) (hedge : edge ∉ d.adjacentCutIndices) : ∃ (g : d.InsideBlockGap), d.insideBlockGapAdjacentIndex g = edge

Every adjacency index outside the proper cuts comes from a unique internal block gap.

noncomputable def Anderson4D.RawCollapseData.insideBlockGapEquivNonCut {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.InsideBlockGap ≃ { edge : AdjacentIndex d.insideLength // edge ∉ d.adjacentCutIndices }

Internal gaps of all blocks are canonically equivalent to adjacency indices outside the proper composition cuts.

Equations

• d.insideBlockGapEquivNonCut = Equiv.ofBijective (fun (g : d.InsideBlockGap) => ⟨d.insideBlockGapAdjacentIndex g, ⋯⟩) ⋯

theorem Anderson4D.RawCollapseData.prod_ite_adjacentCutIndices_eq_prod_insideBlockGap {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (f : AdjacentIndex d.insideLength → ℝ) : (∏ edge : AdjacentIndex d.insideLength, if edge ∈ d.adjacentCutIndices then 1 else f edge) = ∏ g : d.InsideBlockGap, f (d.insideBlockGapAdjacentIndex g)

Reindex a cut-exception product by the internal gaps of the composition blocks.

theorem Anderson4D.RawCollapseData.listChainProduct_block_eq_indexed {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (edge : A ⊕ B → A ⊕ B → ℝ) (i : Fin d.blockComposition.length) : listChainProduct edge (List.map Sum.inl (d.blocks.get ⟨↑i, ⋯⟩)) = indexedChainProduct (fun (a b : A) => edge (Sum.inl a) (Sum.inl b)) (d.insideBlockWord i)

The chain product of a recorded block is the indexed chain product of that block as read from the flattened inside word.

theorem Anderson4D.RawCollapseData.insideBlockChainProduct_eq_prod_insideBlockGap {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (edge : A ⊕ B → A ⊕ B → ℝ) : insideBlockChainProduct edge d = ∏ g : d.InsideBlockGap, edge (Sum.inl (d.insideWord (d.insideBlockGapLeft g))) (Sum.inl (d.insideWord (d.insideBlockGapRight g)))

The product of all recorded inside-block chains, reindexed by the internal gaps of the block composition.

Tree-facing connector

theorem Anderson4D.RawCollapseData.insideBlockChainProduct_originalCollapseEdge_eq_heppChainWeightExcept {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : insideBlockChainProduct (originalCollapseEdge z) d = heppChainWeightExcept (restrictEmbedding z r) d.adjacentCutIndices (restrictedInsideWord r d)

The internal block factor in the expanded lattice chain is exactly the restricted-tree Hepp chain with the proper composition cuts omitted.