Finite-word collapse data for the Proposition 5.9 induction

This file upgrades the list-level collapse equivalence in PermSum/Words.lean to the actual finite words used by validWords.

There are two deliberately separate stages.

• finWordRawCollapseEquiv remembers the maximal inside blocks and the collapsed outside word. Its codomain records the original length, so this is an equivalence for Fin n-indexed words rather than merely for lists.
• The flattened inside word π₁, its composition, the proper cut set O, and the collapsed word π₂ are canonical projections of that data.

No cardinality or quotient argument occurs here: reconstruction is by List.splitWrtComposition followed by expand.

@[reducible, inline]

abbrev Anderson4D.RawCollapseData (A : Type u_3) (B : Type u_4) : Type (max 0 u_3 u_4)

The codomain already used by wordCollapseEquiv, now given a reusable name.

Equations

• Anderson4D.RawCollapseData A B = { p : List (List A) × List (Unit ⊕ B) // (∀ blk ∈ p.1, blk ≠ []) ∧ Anderson4D.markerCount p.2 = p.1.length ∧ Anderson4D.NoTwoAdjacentMarkers p.2 }

def Anderson4D.RawCollapseData.blocks {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List (List A)

The maximal inside blocks.

Equations

• d.blocks = (↑d).1

def Anderson4D.RawCollapseData.collapsed {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List (Unit ⊕ B)

The word in which each maximal inside block is replaced by a marker.

Equations

• d.collapsed = (↑d).2

def Anderson4D.RawCollapseData.expandWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List (A ⊕ B)

Reconstruct the uncollapsed list.

Equations

• d.expandWord = Anderson4D.expand d.blocks d.collapsed

def Anderson4D.RawCollapseData.expandedLength {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : ℕ

The length before collapse.

Equations

• d.expandedLength = d.expandWord.length

def Anderson4D.RawCollapseData.insideList {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List A

The inside letters, with the maximal blocks concatenated in order.

Equations

• d.insideList = d.blocks.flatten

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

The number of inside letters.

Equations

• d.insideLength = d.insideList.length

def Anderson4D.RawCollapseData.blockComposition {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Composition d.insideLength

The composition recording the lengths of the maximal inside blocks.

Equations

• d.blockComposition = { blocks := List.map List.length d.blocks, blocks_pos := ⋯, blocks_sum := ⋯ }

@[simp]

theorem Anderson4D.RawCollapseData.blockComposition_blocks {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.blockComposition.blocks = List.map List.length d.blocks

@[simp]

theorem Anderson4D.RawCollapseData.blockComposition_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.blockComposition.length = d.blocks.length

@[simp]

theorem Anderson4D.RawCollapseData.split_insideList_blockComposition {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.insideList.splitWrtComposition d.blockComposition = d.blocks

Splitting π₁ at the recorded composition cuts recovers the maximal inside blocks in order.

def Anderson4D.RawCollapseData.insideWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Fin d.insideLength → A

The inside word π₁, indexed by its finite length.

Equations

• d.insideWord = List.Vector.get ⟨d.insideList, ⋯⟩

def Anderson4D.RawCollapseData.collapsedWord {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Fin d.collapsed.length → Unit ⊕ B

The collapsed word π₂, indexed by its finite length.

Equations

• d.collapsedWord = List.Vector.get ⟨d.collapsed, ⋯⟩

def Anderson4D.RawCollapseData.markerPositions {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Finset (Fin d.collapsed.length)

Marker positions in π₂. There is one marker per inside block.

These are not the paper's cut set O: their cardinality is the number of blocks, whereas O contains the proper cuts and has one fewer element.

Equations

• d.markerPositions = {i : Fin d.collapsed.length | (d.collapsedWord i).isLeft = true}

@[simp]

theorem Anderson4D.RawCollapseData.mem_markerPositions_iff {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (i : Fin d.collapsed.length) : i ∈ d.markerPositions ↔ (d.collapsedWord i).isLeft = true

theorem Anderson4D.RawCollapseData.card_markerPositions {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.markerPositions.card = d.blocks.length

There is one marker position for every maximal inside block.

theorem Anderson4D.RawCollapseData.card_markerPositions_eq_composition_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.markerPositions.card = d.blockComposition.length

Equivalently, the marker set has the length of the block composition.

def Anderson4D.RawCollapseData.cutEmbedding {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Fin (d.blockComposition.length - 1) ↪ Fin (d.insideLength - 1)

The embedding of proper composition cuts into the gaps of π₁.

The value is the zero-based index of the letter immediately before the cut: the proper partial sum after block i, minus one.

Equations

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

@[simp]

theorem Anderson4D.RawCollapseData.cutEmbedding_val {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (i : Fin (d.blockComposition.length - 1)) : ↑(d.cutEmbedding i) = d.blockComposition.sizeUpTo (↑i + 1) - 1

def Anderson4D.RawCollapseData.cutIndices {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : Finset (Fin (d.insideLength - 1))

The paper's selected cut set O: the proper partial sums of the block composition, represented as gaps of π₁.

Equations

• d.cutIndices = Finset.map d.cutEmbedding Finset.univ

theorem Anderson4D.RawCollapseData.mem_cutIndices_iff {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (j : Fin (d.insideLength - 1)) : j ∈ d.cutIndices ↔ ∃ (i : Fin (d.blockComposition.length - 1)), d.cutEmbedding i = j

@[simp]

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

The degenerate-case-safe cut count: zero blocks and one block both have no proper cuts.

theorem Anderson4D.RawCollapseData.card_cutIndices_add_min_one {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.cutIndices.card + min 1 d.blocks.length = d.blocks.length

Universal cut ledger, including the zero-block degeneration.

theorem Anderson4D.RawCollapseData.card_cutIndices_add_one {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (hblocks : d.blocks ≠ []) : d.cutIndices.card + 1 = d.blocks.length

In the nonempty case used in §5.4.1, |O| + 1 is the number of inside blocks (the paper's s + 1).

@[simp]

theorem Anderson4D.RawCollapseData.expandWord_eq {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.expandWord = expand d.blocks d.collapsed

The original word is recovered by inserting the composition blocks into the marker occurrences of the compound letter, in order.

@[reducible, inline]

abbrev Anderson4D.FixedRawCollapseData (A : Type u_3) (B : Type u_4) (n : ℕ) : Type (max 0 u_3 u_4)

Raw collapse data whose expansion has the prescribed finite length.

Equations

• Anderson4D.FixedRawCollapseData A B n = { d : Anderson4D.RawCollapseData A B // d.expandedLength = n }

def Anderson4D.finWordVectorEquiv (α : Type u_3) (n : ℕ) : (Fin n → α) ≃ List.Vector α n

Fixed-length lists are finite words.

Equations

• Anderson4D.finWordVectorEquiv α n = (Equiv.vectorEquivFin α n).symm

def Anderson4D.vectorRawCollapseEquiv (A : Type u_3) (B : Type u_4) (n : ℕ) : List.Vector (A ⊕ B) n ≃ FixedRawCollapseData A B n

Restrict wordCollapseEquiv to vectors of a fixed length.

Equations

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

def Anderson4D.finWordRawCollapseEquiv (A : Type u_3) (B : Type u_4) (n : ℕ) : (Fin n → A ⊕ B) ≃ FixedRawCollapseData A B n

Finite raw collapse equivalence. This lifts the list equivalence to the Fin n → A ⊕ B carrier of validWords.

Equations

• Anderson4D.finWordRawCollapseEquiv A B n = (Anderson4D.finWordVectorEquiv (A ⊕ B) n).trans (Anderson4D.vectorRawCollapseEquiv A B n)

@[simp]

theorem Anderson4D.finWordRawCollapseEquiv_expandedLength {A : Type u_1} {B : Type u_2} {n : ℕ} (w : Fin n → A ⊕ B) : (↑((finWordRawCollapseEquiv A B n) w)).expandedLength = n

Length transport is part of the finite equivalence's codomain.

@[simp]

theorem Anderson4D.finWordRawCollapseEquiv_expandWord {A : Type u_1} {B : Type u_2} {n : ℕ} (w : Fin n → A ⊕ B) : (↑((finWordRawCollapseEquiv A B n) w)).expandWord = List.ofFn w

The list reconstructed from the finite collapse coordinates is exactly the list underlying the original finite word.

def Anderson4D.finWordCollapseEquiv (A : Type u_3) (B : Type u_4) (n : ℕ) : (Fin n → A ⊕ B) ≃ FixedRawCollapseData A B n

Finite (π₁, O, π₂) collapse equivalence.

The codomain stores the maximal blocks; insideWord, blockComposition, cutIndices, and collapsedWord are its canonical (π₁, O, π₂) coordinates. The inverse inserts the blocks at the marker occurrences of π₂ in order.

Equations

• Anderson4D.finWordCollapseEquiv A B n = Anderson4D.finWordRawCollapseEquiv A B n

Length and multiplicity transport

def Anderson4D.CollapseMultiplicitySpec {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) : Prop

Multiplicity specification on raw collapse data. Inside counts are summed over the composition blocks; outside counts are read from π₂.

Equations

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

theorem Anderson4D.count_inl_ofFn_eq_fiberCard {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (w : Fin n → A ⊕ B) (a : A) : List.count (Sum.inl a) (List.ofFn w) = {i : Fin n | w i = Sum.inl a}.card

Count an inside letter in a finite sum-word by counting its index fiber.

theorem Anderson4D.count_inr_ofFn_eq_fiberCard {A : Type u_1} {B : Type u_2} [DecidableEq A] [DecidableEq B] {n : ℕ} (w : Fin n → A ⊕ B) (b : B) : List.count (Sum.inr b) (List.ofFn w) = {i : Fin n | w i = Sum.inr b}.card

Count an outside letter in a finite sum-word by counting its index fiber.

theorem Anderson4D.mem_validWords_iff_collapseMultiplicitySpec {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (w : Fin n → A ⊕ B) : w ∈ validWords mult ↔ CollapseMultiplicitySpec mult ((wordCollapseEquiv A B) (List.ofFn w))

validWords transports exactly to the inside-block and outside-word multiplicity conditions.

theorem Anderson4D.mem_validWords_iff_finWordRawCollapseSpec {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (w : Fin n → A ⊕ B) : w ∈ validWords mult ↔ CollapseMultiplicitySpec mult ↑((finWordRawCollapseEquiv A B n) w)

The same transport stated directly through the finite raw equivalence.