Chain-product decomposition for the Proposition 5.9 collapse

This file proves the list-level core of paper (5.43). An expanded word is split into nonempty tagged segments: a singleton for every outside letter and one inside block for every marker. Its chain product factors exactly into internal segment products and boundary products. Only boundaries incident to a marker may change under collapse.

Generic nonempty-segment calculus

structure Anderson4D.ChainSegment (X : Type u_4) (Y : Type u_5) : Type (max u_4 u_5)

A nonempty chain segment carrying the letter used to represent it after collapse.

• tag : Y
• letters : List X
• nonempty : self.letters ≠ []

def Anderson4D.ChainSegment.first {X : Type u_1} {Y : Type u_2} (s : ChainSegment X Y) : X

First letter of a nonempty segment.

Equations

• s.first = s.letters.head ⋯

def Anderson4D.ChainSegment.last {X : Type u_1} {Y : Type u_2} (s : ChainSegment X Y) : X

Final letter of a nonempty segment.

Equations

• s.last = s.letters.getLast ⋯

@[simp]

theorem Anderson4D.ChainSegment.first_mk {X : Type u_1} {Y : Type u_2} (tag : Y) (x : X) (xs : List X) : { tag := tag, letters := x :: xs, nonempty := ⋯ }.first = x

def Anderson4D.segmentBoundaryEdge {X : Type u_1} {Y : Type u_2} {R : Type u_3} (edge : X → X → R) (p q : ChainSegment X Y) : R

Chain product across the boundary between two nonempty segments.

Equations

• Anderson4D.segmentBoundaryEdge edge p q = edge p.last q.first

def Anderson4D.flattenSegments {X : Type u_1} {Y : Type u_2} (segments : List (ChainSegment X Y)) : List X

Flatten the letters of a list of nonempty segments.

Equations

• Anderson4D.flattenSegments segments = (List.map Anderson4D.ChainSegment.letters segments).flatten

def Anderson4D.internalSegmentProduct {X : Type u_1} {Y : Type u_2} {R : Type u_3} [Monoid R] (edge : X → X → R) (segments : List (ChainSegment X Y)) : R

Product of the chain products internal to each segment.

Equations

• Anderson4D.internalSegmentProduct edge segments = (List.map (fun (s : Anderson4D.ChainSegment X Y) => Anderson4D.listChainProduct edge s.letters) segments).prod

theorem Anderson4D.listChainProduct_flattenSegments {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommMonoid R] (edge : X → X → R) (segments : List (ChainSegment X Y)) : listChainProduct edge (flattenSegments segments) = internalSegmentProduct edge segments * listChainProduct (segmentBoundaryEdge edge) segments

Exact factorization of a flattened segmented chain into all internal segment chains and the chain of segment-boundary edges.

theorem Anderson4D.listChainProduct_nonneg {α : Type u_4} (edge : α → α → ℝ) (hedge : ∀ (x y : α), 0 ≤ edge x y) (l : List α) : 0 ≤ listChainProduct edge l

Nonnegativity of a real-valued list chain product.

theorem Anderson4D.listChainProduct_le_of_isChain {α : Type u_4} (f g : α → α → ℝ) (hf : ∀ (x y : α), 0 ≤ f x y) (hg : ∀ (x y : α), 0 ≤ g x y) (l : List α) : List.IsChain (fun (x y : α) => f x y ≤ g x y) l → listChainProduct f l ≤ listChainProduct g l

Pointwise comparison on adjacent pairs compares the two chain products.

Marker-boundary ledger

def Anderson4D.markerIndicator {B : Type u_4} : Unit ⊕ B → ℕ

Natural indicator that a collapsed letter is the marker.

Equations

• Anderson4D.markerIndicator (Sum.inl val) = 1
• Anderson4D.markerIndicator (Sum.inr val) = 0

def Anderson4D.markerBoundaryIndicator {B : Type u_4} (x y : Unit ⊕ B) : ℕ

Natural indicator that a collapsed edge is incident to a marker.

Equations

• Anderson4D.markerBoundaryIndicator x y = if x.isLeft = true ∨ y.isLeft = true then 1 else 0

def Anderson4D.markerBoundaryCount {B : Type u_4} : List (Unit ⊕ B) → ℕ

Number of changed boundaries in a collapsed word.

Equations

• Anderson4D.markerBoundaryCount [] = 0
• Anderson4D.markerBoundaryCount [head] = 0
• Anderson4D.markerBoundaryCount (x_1 :: y :: rest) = Anderson4D.markerBoundaryIndicator x_1 y + Anderson4D.markerBoundaryCount (y :: rest)

theorem Anderson4D.markerBoundaryCount_le_two_mul_markerCount {B : Type u_4} (s : List (Unit ⊕ B)) : markerBoundaryCount s ≤ 2 * markerCount s

A path has at most two marker-incident boundaries per marker. The endpoint-inclusive convention used here gives the bound 2(s+1).

theorem Anderson4D.listChainProduct_markerBoundaryCost {B : Type u_4} (edge : Unit ⊕ B → Unit ⊕ B → ℝ) (s : List (Unit ⊕ B)) : listChainProduct (fun (x y : Unit ⊕ B) => 2 ^ markerBoundaryIndicator x y * edge x y) s = 2 ^ markerBoundaryCount s * listChainProduct edge s

Replacing every marker-incident edge factor by twice its collapsed counterpart extracts exactly one factor 2 per changed boundary.

theorem Anderson4D.segmentBoundaryProduct_le_markerCost {X : Type u_1} {B : Type u_4} (edge : X → X → ℝ) (collapsedEdge : Unit ⊕ B → Unit ⊕ B → ℝ) (segments : List (ChainSegment X (Unit ⊕ B))) (hedge : ∀ (x y : X), 0 ≤ edge x y) (hcollapsed : ∀ (x y : Unit ⊕ B), 0 ≤ collapsedEdge x y) (hcompare : List.IsChain (fun (p q : ChainSegment X (Unit ⊕ B)) => segmentBoundaryEdge edge p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedEdge p.tag q.tag) segments) : listChainProduct (segmentBoundaryEdge edge) segments ≤ 2 ^ markerBoundaryCount (List.map ChainSegment.tag segments) * listChainProduct collapsedEdge (List.map ChainSegment.tag segments)

Generic boundary comparison for tagged segments.

theorem Anderson4D.internalSegmentProduct_nonneg {X : Type u_1} {Y : Type u_2} (edge : X → X → ℝ) (hedge : ∀ (x y : X), 0 ≤ edge x y) (segments : List (ChainSegment X Y)) : 0 ≤ internalSegmentProduct edge segments

theorem Anderson4D.listChainProduct_flattenSegments_le_four_pow {X : Type u_1} {B : Type u_4} (edge : X → X → ℝ) (collapsedEdge : Unit ⊕ B → Unit ⊕ B → ℝ) (segments : List (ChainSegment X (Unit ⊕ B))) (hedge : ∀ (x y : X), 0 ≤ edge x y) (hcollapsed : ∀ (x y : Unit ⊕ B), 0 ≤ collapsedEdge x y) (hcompare : List.IsChain (fun (p q : ChainSegment X (Unit ⊕ B)) => segmentBoundaryEdge edge p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedEdge p.tag q.tag) segments) : listChainProduct edge (flattenSegments segments) ≤ 4 ^ markerCount (List.map ChainSegment.tag segments) * internalSegmentProduct edge segments * listChainProduct collapsedEdge (List.map ChainSegment.tag segments)

Segmented-chain estimate with the corrected 4^(number of markers) loss.

Segments canonically attached to raw collapse data

def Anderson4D.collapseSegmentsAux {A : Type u_4} {B : Type u_5} (bs : List (List A)) (collapsed : List (Unit ⊕ B)) : (∀ block ∈ bs, block ≠ []) → List (ChainSegment (A ⊕ B) (Unit ⊕ B))

Turn expand bs collapsed into nonempty tagged segments. A marker with no remaining block is silently dropped, matching expand; raw collapse data exclude that degeneration by their marker-count invariant.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.collapseSegmentsAux x [] x_1 = []
• Anderson4D.collapseSegmentsAux x (Sum.inr b :: collapsed) x_1 = { tag := Sum.inr b, letters := [Sum.inr b], nonempty := ⋯ } :: Anderson4D.collapseSegmentsAux x collapsed x_1
• Anderson4D.collapseSegmentsAux [] (Sum.inl val :: collapsed) x_3 = Anderson4D.collapseSegmentsAux [] collapsed ⋯

theorem Anderson4D.flattenSegments_collapseSegmentsAux {A : Type u_4} {B : Type u_5} (bs : List (List A)) (collapsed : List (Unit ⊕ B)) (hbs : ∀ block ∈ bs, block ≠ []) : flattenSegments (collapseSegmentsAux bs collapsed hbs) = expand bs collapsed

The segment letters flatten to the definition of expand.

theorem Anderson4D.map_tag_collapseSegmentsAux {A : Type u_4} {B : Type u_5} (bs : List (List A)) (collapsed : List (Unit ⊕ B)) (hbs : ∀ block ∈ bs, block ≠ []) : markerCount collapsed = bs.length → List.map ChainSegment.tag (collapseSegmentsAux bs collapsed hbs) = collapsed

With exact marker bookkeeping, segment tags recover the collapsed word.

theorem Anderson4D.internalProduct_collapseSegmentsAux {A : Type u_4} {B : Type u_5} (edge : A ⊕ B → A ⊕ B → ℝ) (bs : List (List A)) (collapsed : List (Unit ⊕ B)) (hbs : ∀ block ∈ bs, block ≠ []) : markerCount collapsed = bs.length → internalSegmentProduct edge (collapseSegmentsAux bs collapsed hbs) = (List.map (fun (block : List A) => listChainProduct edge (List.map Sum.inl block)) bs).prod

Internal segment factors are exactly the products internal to the inside blocks; outside singleton segments contribute one.

def Anderson4D.RawCollapseData.chainSegments {A : Type u_4} {B : Type u_5} (d : RawCollapseData A B) : List (ChainSegment (A ⊕ B) (Unit ⊕ B))

Canonical nonempty segments of raw collapse data.

Equations

• d.chainSegments = Anderson4D.collapseSegmentsAux d.blocks d.collapsed ⋯

@[simp]

theorem Anderson4D.RawCollapseData.flatten_chainSegments {A : Type u_4} {B : Type u_5} (d : RawCollapseData A B) : flattenSegments d.chainSegments = d.expandWord

@[simp]

theorem Anderson4D.RawCollapseData.map_tag_chainSegments {A : Type u_4} {B : Type u_5} (d : RawCollapseData A B) : List.map ChainSegment.tag d.chainSegments = d.collapsed

def Anderson4D.RawCollapseData.insideBlockChainProduct {A : Type u_4} {B : Type u_5} (edge : A ⊕ B → A ⊕ B → ℝ) (d : RawCollapseData A B) : ℝ

Product of the chain weights internal to all inside blocks.

Equations

• Anderson4D.RawCollapseData.insideBlockChainProduct edge d = (List.map (fun (block : List A) => Anderson4D.listChainProduct edge (List.map Sum.inl block)) d.blocks).prod

@[simp]

theorem Anderson4D.RawCollapseData.internalProduct_chainSegments {A : Type u_4} {B : Type u_5} (edge : A ⊕ B → A ⊕ B → ℝ) (d : RawCollapseData A B) : internalSegmentProduct edge d.chainSegments = insideBlockChainProduct edge d

theorem Anderson4D.RawCollapseData.expandWord_chain_le_four_pow_blocks {A : Type u_4} {B : Type u_5} (edge : A ⊕ B → A ⊕ B → ℝ) (collapsedEdge : Unit ⊕ B → Unit ⊕ B → ℝ) (d : RawCollapseData A B) (hedge : ∀ (x y : A ⊕ B), 0 ≤ edge x y) (hcollapsed : ∀ (x y : Unit ⊕ B), 0 ≤ collapsedEdge x y) (hcompare : List.IsChain (fun (p q : ChainSegment (A ⊕ B) (Unit ⊕ B)) => segmentBoundaryEdge edge p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedEdge p.tag q.tag) d.chainSegments) : listChainProduct edge d.expandWord ≤ 4 ^ d.blocks.length * insideBlockChainProduct edge d * listChainProduct collapsedEdge d.collapsed

Raw-coordinate form of (5.43), with the local changed-boundary comparison exposed as an IsChain hypothesis.

theorem Anderson4D.RawCollapseData.expandWord_chain_le_four_pow_insideLength {A : Type u_4} {B : Type u_5} (edge : A ⊕ B → A ⊕ B → ℝ) (collapsedEdge : Unit ⊕ B → Unit ⊕ B → ℝ) (d : RawCollapseData A B) (hedge : ∀ (x y : A ⊕ B), 0 ≤ edge x y) (hcollapsed : ∀ (x y : Unit ⊕ B), 0 ≤ collapsedEdge x y) (hcompare : List.IsChain (fun (p q : ChainSegment (A ⊕ B) (Unit ⊕ B)) => segmentBoundaryEdge edge p q ≤ 2 ^ markerBoundaryIndicator p.tag q.tag * collapsedEdge p.tag q.tag) d.chainSegments) : listChainProduct edge d.expandWord ≤ 4 ^ d.insideLength * insideBlockChainProduct edge d * listChainProduct collapsedEdge d.collapsed

Paper's coarser 4^n form, where n is the total inside length.