Typed coordinates for the Proposition 5.9 collapse

This module records the length and multiplicity ledgers carried by the finite-word collapse, and exposes the change of variables

raw collapse data ≃ (inside list, positive composition, collapsed list).

The last item is an actual Equiv: the block list is recovered by splitting the inside list at the composition boundaries. In particular, none of the coordinate projections is used as though it were injective.

theorem Anderson4D.RawCollapseData.expandedLength_add_blocks_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.expandedLength + d.blocks.length = d.insideLength + d.collapsed.length

Exact additive length ledger before solving for the collapsed length.

theorem Anderson4D.RawCollapseData.insideLength_le_expandedLength {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.insideLength ≤ d.expandedLength

Every inside letter survives expansion.

theorem Anderson4D.RawCollapseData.collapsed_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.collapsed.length = d.expandedLength - d.insideLength + d.blocks.length

The collapsed word has the paper's length expanded length - inside length + number of blocks.

theorem Anderson4D.RawCollapseData.collapsed_length_fixed {A : Type u_1} {B : Type u_2} {n : ℕ} (d : FixedRawCollapseData A B n) : (↑d).collapsed.length = n - (↑d).insideLength + (↑d).blocks.length

Fixed-original-length form of collapsed_length.

Multiplicity transport to the two coordinate words

def Anderson4D.insideMultiplicity {A : Type u_1} {B : Type u_2} (mult : A ⊕ B → ℕ) : A → ℕ

Multiplicity of an inside letter in π₁.

Equations

• Anderson4D.insideMultiplicity mult a = mult (Sum.inl a)

def Anderson4D.collapsedMultiplicity {A : Type u_1} {B : Type u_2} (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) : Unit ⊕ B → ℕ

Multiplicity in π₂: the new marker occurs once for each inside block, while every outside multiplicity is unchanged.

Equations

• Anderson4D.collapsedMultiplicity mult d (Sum.inl val) = d.blocks.length
• Anderson4D.collapsedMultiplicity mult d (Sum.inr b) = mult (Sum.inr b)

theorem Anderson4D.RawCollapseData.insideWord_mem_validWords {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : d.insideWord ∈ validWords (insideMultiplicity mult)

π₁ has exactly the inside multiplicities prescribed by the original word.

theorem Anderson4D.RawCollapseData.collapsedWord_mem_validWords {A : Type u_1} {B : Type u_2} [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : d.collapsedWord ∈ validWords (collapsedMultiplicity mult d)

π₂ has one marker per inside block and preserves every outside multiplicity.

theorem Anderson4D.RawCollapseData.sum_insideMultiplicity_eq_insideLength {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : ∑ a : A, insideMultiplicity mult a = d.insideLength

Total inside multiplicity is the length of π₁.

theorem Anderson4D.RawCollapseData.sum_collapsedMultiplicity_eq_collapsed_length {A : Type u_1} {B : Type u_2} [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : ∑ x : Unit ⊕ B, collapsedMultiplicity mult d x = d.collapsed.length

Total collapsed multiplicity is the length of π₂.

theorem Anderson4D.RawCollapseData.sum_collapsedMultiplicity_eq_length_ledger {A : Type u_1} {B : Type u_2} [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : ∑ x : Unit ⊕ B, collapsedMultiplicity mult d x = d.expandedLength - d.insideLength + d.blocks.length

The total π₂ multiplicity in original-length coordinates.

theorem Anderson4D.RawCollapseData.sum_collapsedMultiplicity_eq_fixed_length_ledger {A : Type u_1} {B : Type u_2} [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {n : ℕ} {d : FixedRawCollapseData A B n} (h : CollapseMultiplicitySpec mult ↑d) : ∑ x : Unit ⊕ B, collapsedMultiplicity mult (↑d) x = n - (↑d).insideLength + (↑d).blocks.length

Fixed-original-length form of the total π₂ multiplicity ledger.

Genuine (π₁, composition, π₂) coordinates

structure Anderson4D.CollapseCoordinates (A : Type u_3) (B : Type u_4) : Type (max u_3 u_4)

Typed collapse coordinates. compositionBlocks together with its two certificates is exactly a positive composition of inside.length; keeping its data fields exposed makes equality of coordinates proof-irrelevant.

• inside : List A

  The flattened inside word π₁.

• compositionBlocks : List ℕ

  Positive block lengths, i.e. the composition between π₁ and π₂.

• compositionBlocks_pos {k : ℕ} : k ∈ self.compositionBlocks → 0 < k
• compositionBlocks_sum : self.compositionBlocks.sum = self.inside.length
• collapsed : List (Unit ⊕ B)

  The collapsed outside word π₂.

• marker_count : markerCount self.collapsed = self.compositionBlocks.length
• noTwoAdjacentMarkers : NoTwoAdjacentMarkers self.collapsed

theorem Anderson4D.CollapseCoordinates.ext {A : Type u_3} {B : Type u_4} {x y : CollapseCoordinates A B} (inside : x.inside = y.inside) (compositionBlocks : x.compositionBlocks = y.compositionBlocks) (collapsed : x.collapsed = y.collapsed) : x = y

theorem Anderson4D.CollapseCoordinates.ext_iff {A : Type u_3} {B : Type u_4} {x y : CollapseCoordinates A B} : x = y ↔ x.inside = y.inside ∧ x.compositionBlocks = y.compositionBlocks ∧ x.collapsed = y.collapsed

def Anderson4D.CollapseCoordinates.composition {A : Type u_1} {B : Type u_2} (q : CollapseCoordinates A B) : Composition q.inside.length

The genuine mathlib Composition carried by the coordinate block lengths.

Equations

• q.composition = { blocks := q.compositionBlocks, blocks_pos := ⋯, blocks_sum := ⋯ }

@[simp]

theorem Anderson4D.CollapseCoordinates.composition_blocks {A : Type u_1} {B : Type u_2} (q : CollapseCoordinates A B) : q.composition.blocks = q.compositionBlocks

@[simp]

theorem Anderson4D.CollapseCoordinates.composition_length {A : Type u_1} {B : Type u_2} (q : CollapseCoordinates A B) : q.composition.length = q.compositionBlocks.length

def Anderson4D.collapseCoordinatesToRaw {A : Type u_1} {B : Type u_2} (q : CollapseCoordinates A B) : RawCollapseData A B

Forget the explicit coordinates by splitting π₁ at the composition boundaries.

Equations

• Anderson4D.collapseCoordinatesToRaw q = ⟨(q.inside.splitWrtComposition q.composition, q.collapsed), ⋯⟩

def Anderson4D.rawToCollapseCoordinates {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : CollapseCoordinates A B

Read the flattened inside word, its block composition, and the collapsed word from raw collapse data.

Equations

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

def Anderson4D.rawCollapseCoordinatesEquiv (A : Type u_3) (B : Type u_4) : RawCollapseData A B ≃ CollapseCoordinates A B

Raw block/collapsed data are equivalent to the explicit (π₁, composition, π₂) coordinates.

Equations

• Anderson4D.rawCollapseCoordinatesEquiv A B = { toFun := Anderson4D.rawToCollapseCoordinates, invFun := Anderson4D.collapseCoordinatesToRaw, left_inv := ⋯, right_inv := ⋯ }