Predicate transport for the Proposition 5.9 word collapse

This file proves the logical side-condition transport used in the collapse step of §5.4.1. The proper composition cuts are first identified with AdjacentIndex; adjacency is then transported both to the flattened inside word (away from those cuts) and to the collapsed outside word.

The inside alphabet

def Anderson4D.insideAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] : Finset (A ⊕ B)

The original letters belonging to the selected subtree.

Equations

• Anderson4D.insideAlphabet = Finset.image Sum.inl Finset.univ

@[simp]

theorem Anderson4D.inl_mem_insideAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (a : A) : Sum.inl a ∈ insideAlphabet

@[simp]

theorem Anderson4D.inr_not_mem_insideAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (b : B) : Sum.inr b ∉ insideAlphabet

theorem Anderson4D.insideAlphabet_nonempty {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [DecidableEq A] [DecidableEq B] : insideAlphabet.Nonempty

theorem Anderson4D.insideAlphabet_ssubset_univ {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty B] [DecidableEq A] [DecidableEq B] : insideAlphabet ⊂ Finset.univ

Finite-word/list bridges

def Anderson4D.finPredEquivAdjacentIndex (n : ℕ) : Fin (n - 1) ≃ AdjacentIndex n

Gaps of a word of length n and the project's adjacency indices are the same finite type.

Equations

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

@[simp]

theorem Anderson4D.finPredEquivAdjacentIndex_val (n : ℕ) (i : Fin (n - 1)) : ↑↑((finPredEquivAdjacentIndex n) i) = ↑i

@[simp]

theorem Anderson4D.finPredEquivAdjacentIndex_symm_val (n : ℕ) (i : AdjacentIndex n) : ↑((finPredEquivAdjacentIndex n).symm i) = ↑↑i

theorem Anderson4D.noAdjacentEqual_iff_isChain_ofFn {α : Type u_3} {n : ℕ} (w : Fin n → α) : NoAdjacentEqual w ↔ List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) (List.ofFn w)

NoAdjacentEqual is exactly the ordinary unequal-neighbour chain condition on the list underlying a finite word.

def Anderson4D.RawCollapseData.adjacentCutIndices {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Finset (AdjacentIndex d.insideLength)

The paper cut set on the exact carrier expected by Proposition 5.10.

Equations

• d.adjacentCutIndices = Finset.map (Anderson4D.finPredEquivAdjacentIndex d.insideLength).toEmbedding d.cutIndices

theorem Anderson4D.RawCollapseData.mem_adjacentCutIndices_iff {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (j : AdjacentIndex d.insideLength) : j ∈ d.adjacentCutIndices ↔ (finPredEquivAdjacentIndex d.insideLength).symm j ∈ d.cutIndices

@[simp]

theorem Anderson4D.RawCollapseData.card_adjacentCutIndices {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.adjacentCutIndices.card = d.blocks.length - 1

@[simp]

theorem Anderson4D.RawCollapseData.ofFn_insideWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List.ofFn d.insideWord = d.insideList

@[simp]

theorem Anderson4D.RawCollapseData.ofFn_collapsedWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List.ofFn d.collapsedWord = d.collapsed

List-level collapse lemmas

theorem Anderson4D.collapse_collapsed_isChain_ne {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (w : List (A ⊕ B)) : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) w → List.IsChain (fun (x1 x2 : Unit ⊕ B) => x1 ≠ x2) (collapse w).2

Collapsing maximal inside runs preserves unequal adjacency in the collapsed word.

theorem Anderson4D.collapse_blocks_isChain_ne {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (w : List (A ⊕ B)) : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) w → ∀ blk ∈ (collapse w).1, List.IsChain (fun (x1 x2 : A) => x1 ≠ x2) blk

Every maximal inside block inherits unequal adjacency from the original word.

The one-block degeneration

theorem Anderson4D.markerCount_eq_zero_iff_exists_map_inr {B : Type u_2} (s : List (Unit ⊕ B)) : markerCount s = 0 ↔ ∃ (bs : List B), s = List.map Sum.inr bs

A collapsed list has no marker exactly when every entry is an outside letter.

theorem Anderson4D.markerCount_eq_one_decompose {B : Type u_2} (s : List (Unit ⊕ B)) (h : markerCount s = 1) : ∃ (pre : List B) (post : List B), s = List.map Sum.inr pre ++ [Sum.inl ()] ++ List.map Sum.inr post

A collapsed list with one marker is an outside prefix, the unique marker, and an outside suffix.

theorem Anderson4D.expand_single_block_decompose {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (hblocks : d.blocks.length = 1) : ∃ (blk : List A) (pre : List B) (post : List B), blk ≠ [] ∧ d.blocks = [blk] ∧ d.expandWord = List.map Sum.inr pre ++ List.map Sum.inl blk ++ List.map Sum.inr post

If there is one inside block, expansion is an outside prefix followed by that block and an outside suffix.

theorem Anderson4D.RawCollapseData.collapsedWord_noAdjacentEqual {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (h : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) d.expandWord) : NoAdjacentEqual d.collapsedWord

The collapsed outside word inherits the no-equal-neighbours condition from the expanded word.

theorem Anderson4D.RawCollapseData.blocks_isChain_ne {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (h : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) d.expandWord) (blk : List A) : blk ∈ d.blocks → List.IsChain (fun (x1 x2 : A) => x1 ≠ x2) blk

Every recorded inside block inherits the no-equal-neighbours condition from the expanded word.

theorem Anderson4D.RawCollapseData.getElem_block_eq_insideList {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (i j : ℕ) (hi : i < d.blocks.length) (hj : j < d.blocks[i].length) : d.blocks[i][j] = d.insideList.get ⟨d.blockComposition.sizeUpTo i + j, ⋯⟩

Reading a letter from a composition block agrees with reading the flattened inside list at the block offset.

theorem Anderson4D.RawCollapseData.sizeUpTo_ne_succ_of_not_mem_cutIndices {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (j : Fin (d.insideLength - 1)) (hj : j ∉ d.cutIndices) (i : ℕ) (hi : i + 1 < d.blockComposition.length) : d.blockComposition.sizeUpTo (i + 1) ≠ ↑j + 1

A gap outside the canonical cut set is not a proper composition boundary.

theorem Anderson4D.RawCollapseData.insideWord_noAdjacentOutside {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (h : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) d.expandWord) : NoAdjacentOutside d.adjacentCutIndices d.insideWord

The flattened inside word has unequal neighbours away from precisely the proper composition cuts.

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

The cut set is nonempty as soon as the selected inside letters form at least two maximal blocks.

theorem Anderson4D.RawCollapseData.adjacentCutIndices_nonempty_iff {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.adjacentCutIndices.Nonempty ↔ 2 ≤ d.blocks.length

Exact nondegenerate cut-count criterion.

Transport directly from the finite collapse equivalence

theorem Anderson4D.finWordCollapse_expand_isChain {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (w : Fin n → A ⊕ B) (hw : NoAdjacentEqual w) : List.IsChain (fun (x1 x2 : A ⊕ B) => x1 ≠ x2) (↑((finWordCollapseEquiv A B n) w)).expandWord

The original finite word supplies the expanded-list chain hypothesis used by both predicate transports.

theorem Anderson4D.finWordCollapse_insideWord_noAdjacentOutside {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (w : Fin n → A ⊕ B) (hw : NoAdjacentEqual w) : have d := ↑((finWordCollapseEquiv A B n) w); NoAdjacentOutside d.adjacentCutIndices d.insideWord

Finite-word form of the inside predicate transport required before applying Proposition 5.10.

theorem Anderson4D.finWordCollapse_collapsedWord_noAdjacentEqual {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (w : Fin n → A ⊕ B) (hw : NoAdjacentEqual w) : have d := ↑((finWordCollapseEquiv A B n) w); NoAdjacentEqual d.collapsedWord

Finite-word form of the collapsed-word adjacency transport used by the inductive call on the contracted tree.