Primitivity transport through the Proposition 5.9 collapse

This file transports paper condition (5.11)(c), represented by NoProperLeafBlock, through the inside-subtree word collapse.

def Anderson4D.listWord {α : Type u_3} (l : List α) : Fin l.length → α

Canonical finite word associated with a list.

Equations

• Anderson4D.listWord l = List.Vector.get ⟨l, ⋯⟩

@[simp]

theorem Anderson4D.ofFn_listWord {α : Type u_3} (l : List α) : List.ofFn (listWord l) = l

def Anderson4D.RawCollapseData.expandedWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Fin d.expandedLength → A ⊕ B

The finite word represented by the expanded list.

Equations

• d.expandedWord = List.Vector.get ⟨d.expandWord, ⋯⟩

@[simp]

theorem Anderson4D.RawCollapseData.ofFn_expandedWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List.ofFn d.expandedWord = d.expandWord

theorem Anderson4D.RawCollapseData.expandedWord_eq_listWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.expandedWord = listWord d.expandWord

theorem Anderson4D.RawCollapseData.collapsedWord_eq_listWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.collapsedWord = listWord d.collapsed

Pulling a collapsed alphabet subset back before collapse

def Anderson4D.collapseAlphabetMap {A : Type u_1} {B : Type u_2} (x : A ⊕ B) : Unit ⊕ B

A collapsed subset pulls back by replacing the marker with the whole inside alphabet and leaving outside letters unchanged.

Equations

• Anderson4D.collapseAlphabetMap (Sum.inl val) = Sum.inl ()
• Anderson4D.collapseAlphabetMap (Sum.inr b) = Sum.inr b

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

Equations

• Anderson4D.liftCollapsedAlphabet S = {x : A ⊕ B | Anderson4D.collapseAlphabetMap x ∈ S}

@[simp]

theorem Anderson4D.inl_mem_liftCollapsedAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (S : Finset (Unit ⊕ B)) (a : A) : Sum.inl a ∈ liftCollapsedAlphabet S ↔ Sum.inl () ∈ S

@[simp]

theorem Anderson4D.inr_mem_liftCollapsedAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (S : Finset (Unit ⊕ B)) (b : B) : Sum.inr b ∈ liftCollapsedAlphabet S ↔ Sum.inr b ∈ S

theorem Anderson4D.liftCollapsedAlphabet_nonempty {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [DecidableEq A] [DecidableEq B] {S : Finset (Unit ⊕ B)} (hS : S.Nonempty) : (liftCollapsedAlphabet S).Nonempty

theorem Anderson4D.liftCollapsedAlphabet_ssubset_univ {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [DecidableEq A] [DecidableEq B] {S : Finset (Unit ⊕ B)} (hS : S ⊂ Finset.univ) : liftCollapsedAlphabet S ⊂ Finset.univ

Expansion respects synchronized concatenation

theorem Anderson4D.expand_append_of_markerCount {A : Type u_1} {B : Type u_2} (bs₁ bs₂ : List (List A)) (s₁ s₂ : List (Unit ⊕ B)) (hcount : markerCount s₁ = bs₁.length) : expand (bs₁ ++ bs₂) (s₁ ++ s₂) = expand bs₁ s₁ ++ expand bs₂ s₂

Expansion distributes over concatenation when the first collapsed segment consumes exactly the first block segment.

theorem Anderson4D.all_mem_expand_liftCollapsedAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (S : Finset (Unit ⊕ B)) (bs : List (List A)) (s : List (Unit ⊕ B)) (hs : ∀ y ∈ s, y ∈ S) (x : A ⊕ B) : x ∈ expand bs s → x ∈ liftCollapsedAlphabet S

Every expanded letter is selected by the lifted alphabet if all source tokens in the collapsed segment are selected.

theorem Anderson4D.all_not_mem_expand_liftCollapsedAlphabet {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (S : Finset (Unit ⊕ B)) (bs : List (List A)) (s : List (Unit ⊕ B)) (hs : ∀ y ∈ s, y ∉ S) (x : A ⊕ B) : x ∈ expand bs s → x ∉ liftCollapsedAlphabet S

Every expanded letter is unselected by the lifted alphabet if all source tokens in the collapsed segment are unselected.

theorem Anderson4D.expand_ne_nil_of_ne_nil {A : Type u_1} {B : Type u_2} (bs : List (List A)) (s : List (Unit ⊕ B)) (hbs : ∀ blk ∈ bs, blk ≠ []) (hcount : markerCount s = bs.length) (hs : s ≠ []) : expand bs s ≠ []

Under the raw-collapse nonempty-block invariant, a nonempty collapsed segment has a nonempty expansion.

theorem Anderson4D.all_mem_of_letterPositions_eq_univ {α : Type u_3} [Fintype α] [DecidableEq α] (T : Finset α) (l : List α) (hpositions : letterPositions (listWord l) T = Finset.univ) (x : α) : x ∈ l → x ∈ T

If every position of the canonical finite word is selected, every list entry is selected.

A single middle block is an index interval

theorem Anderson4D.get_mem_insideAlphabet_iff_middle_range {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (l : List (A ⊕ B)) (pre : List B) (blk : List A) (post : List B) (hl : l = List.map Sum.inr pre ++ List.map Sum.inl blk ++ List.map Sum.inr post) (i : Fin l.length) : l.get i ∈ insideAlphabet ↔ pre.length ≤ ↑i ∧ ↑i < pre.length + blk.length

In an outside/inside/outside list, membership in the inside alphabet is exactly membership in the middle numerical range. Keeping the ambient list as a variable lets dependent elimination transport its Fin index cleanly.

theorem Anderson4D.get_mem_iff_middle_range_of_forall {α : Type u_3} [DecidableEq α] (T : Finset α) (l pre mid post : List α) (hl : l = pre ++ mid ++ post) (hpre : ∀ x ∈ pre, x ∉ T) (hmid : ∀ x ∈ mid, x ∈ T) (hpost : ∀ x ∈ post, x ∉ T) (i : Fin l.length) : l.get i ∈ T ↔ pre.length ≤ ↑i ∧ ↑i < pre.length + mid.length

Generic form of the middle-range lemma for an arbitrary finite alphabet subset and lists already known to be respectively outside/inside/outside.

theorem Anderson4D.letterPositions_eq_Icc_of_decompose {α : Type u_3} [Fintype α] [DecidableEq α] (T : Finset α) (l pre mid post : List α) (hl : l = pre ++ mid ++ post) (hpre : ∀ x ∈ pre, x ∉ T) (hmid : ∀ x ∈ mid, x ∈ T) (hpost : ∀ x ∈ post, x ∉ T) (hmidNonempty : mid ≠ []) : have w := List.Vector.get ⟨l, ⋯⟩; ∃ (a : Fin l.length) (b : Fin l.length), a ≤ b ∧ letterPositions w T = Finset.Icc a b

An outside/inside/outside list decomposition gives the corresponding closed interval of selected finite-word positions.

theorem Anderson4D.decompose_of_letterPositions_eq_Icc {α : Type u_3} [Fintype α] [DecidableEq α] (T : Finset α) (l : List α) (a b : Fin l.length) (hab : a ≤ b) (hpositions : letterPositions (listWord l) T = Finset.Icc a b) : ∃ (pre : List α) (mid : List α) (post : List α), l = pre ++ mid ++ post ∧ mid ≠ [] ∧ (∀ x ∈ pre, x ∉ T) ∧ (∀ x ∈ mid, x ∈ T) ∧ ∀ x ∈ post, x ∉ T

Conversely, a closed interval of selected finite-word positions yields an outside/inside/outside list decomposition.

theorem Anderson4D.middle_range_eq_Icc (preLength blockLength totalLength : ℕ) (hblock : 0 < blockLength) (hfit : preLength + blockLength ≤ totalLength) : {i : Fin totalLength | preLength ≤ ↑i ∧ ↑i < preLength + blockLength} = Finset.Icc ⟨preLength, ⋯⟩ ⟨preLength + blockLength - 1, ⋯⟩

The middle numerical range is the closed Fin interval from its first to its last position.

theorem Anderson4D.RawCollapseData.letterPositions_insideAlphabet_eq_Icc_of_blocks_length_one {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (hblocks : d.blocks.length = 1) : ∃ (a : Fin d.expandedLength) (b : Fin d.expandedLength), a ≤ b ∧ letterPositions d.expandedWord insideAlphabet = Finset.Icc a b

With one inside block, the positions occupied by inside letters form one closed interval.

Excluding the one-block and zero-block degenerations

theorem Anderson4D.RawCollapseData.blocks_nonempty_of_inside_occurs {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (hinside : ∃ (i : Fin d.expandedLength), d.expandedWord i ∈ insideAlphabet) : d.blocks ≠ []

An actually occurring inside letter forces at least one collapse block.

theorem Anderson4D.RawCollapseData.two_le_blocks_of_noProperLeafBlock {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (hprimitive : NoProperLeafBlock d.expandedWord) (hinside : ∃ (i : Fin d.expandedLength), d.expandedWord i ∈ insideAlphabet) (houtside : ∃ (i : Fin d.expandedLength), d.expandedWord i ∉ insideAlphabet) : 2 ≤ d.blocks.length

The primitivity source of s ≥ 1. If both sides of the alphabet actually occur, condition (5.11)(c) rules out a single maximal inside block. Consequently there are at least two blocks and hence at least one proper composition cut.

theorem Anderson4D.RawCollapseData.two_le_blocks_of_noProperLeafBlock_of_mem_validWords_of_pos {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) (hprimitive : NoProperLeafBlock d.expandedWord) (hvalid : d.expandedWord ∈ validWords mult) (hpos : ∀ (x : A ⊕ B), 0 < mult x) : 2 ≤ d.blocks.length

Valid positive multiplicities discharge the two occurrence hypotheses in two_le_blocks_of_noProperLeafBlock.

theorem Anderson4D.RawCollapseData.one_le_card_adjacentCutIndices_of_mem_validWords_of_pos {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) (hprimitive : NoProperLeafBlock d.expandedWord) (hvalid : d.expandedWord ∈ validWords mult) (hpos : ∀ (x : A ⊕ B), 0 < mult x) : 1 ≤ d.adjacentCutIndices.card

Positive valid multiplicities give the paper's nondegenerate cut ledger 1 ≤ s = |O|.

theorem Anderson4D.RawCollapseData.collapsedWord_noProperLeafBlock {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (hprimitive : NoProperLeafBlock d.expandedWord) : NoProperLeafBlock d.collapsedWord

Primitivity descends to the word on the contracted alphabet. A collapsed alphabet subset is pulled back by replacing the marker with the whole inside alphabet; a collapsed interval expands to an interval before collapse.

theorem Anderson4D.RawCollapseData.one_le_card_adjacentCutIndices_of_noProperLeafBlock {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] [DecidableEq A] [DecidableEq B] (d : RawCollapseData A B) (hprimitive : NoProperLeafBlock d.expandedWord) (hinside : ∃ (i : Fin d.expandedLength), d.expandedWord i ∈ insideAlphabet) (houtside : ∃ (i : Fin d.expandedLength), d.expandedWord i ∉ insideAlphabet) : 1 ≤ d.adjacentCutIndices.card

Equivalent cut-cardinality form used in the paper's notation s = |O|.