Active collapse shapes

The primitive-word condition excludes raw collapse data with fewer than two inside blocks. This module records that exclusion at the level of the outer shape ledger and removes the corresponding zero fibers from the exact fixed-word sum.

theorem Anderson4D.RawCollapseData.expandedWord_mem_validWords_of_collapseMultiplicitySpec {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) (hSpec : CollapseMultiplicitySpec mult d) : d.expandedWord ∈ validWords mult

A raw collapse datum satisfying the multiplicity specification expands to a valid word with those multiplicities.

theorem Anderson4D.RawCollapseData.two_le_blocks_of_splitSpec_of_noProperLeafBlock {t : PlaneTree} (_ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (r : t.VPos) (hr : r ∈ nonrootBranches t) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (hSpec : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) (hprimitive : NoProperLeafBlock d.expandedWord) : 2 ≤ d.blocks.length

In the tree split, positive leaf multiplicities and primitivity force at least two maximal inside blocks.

Active shape family

noncomputable def Anderson4D.activeCollapseShapes {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (M : ℕ) : Finset (List ℕ)

Occurring split-alphabet shapes with at least two blocks.

Equations

• Anderson4D.activeCollapseShapes mu r M = {shape ∈ Anderson4D.validCollapseShapes (Anderson4D.splitLeafMultiplicity mu r) M | 2 ≤ shape.length}

@[simp]

theorem Anderson4D.mem_activeCollapseShapes_iff {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (M : ℕ) (shape : List ℕ) : shape ∈ activeCollapseShapes mu r M ↔ shape ∈ validCollapseShapes (splitLeafMultiplicity mu r) M ∧ 2 ≤ shape.length

Vanishing of inactive shape fibers

theorem Anderson4D.collapseRawFixedWordSummand_eq_zero_of_shape_length_lt_two {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (r : t.VPos) (hr : r ∈ nonrootBranches t) (z : HeppLeaf t → Fin 4 → ℤ) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (shape : List ℕ) (hshape : d.collapseShape = shape) (hsmall : shape.length < 2) : collapseRawFixedWordSummand mu r z lstar d = 0

A fixed-word summand whose collapse shape has fewer than two blocks vanishes.

Exact active-shape decomposition

theorem Anderson4D.sum_collapseRawFixedWordSummand_eq_sum_activeShapes {t : PlaneTree} {M : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (r : t.VPos) (hr : r ∈ nonrootBranches t) (z : HeppLeaf t → Fin 4 → ℤ) (lstar : InsideLeaf r) : ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M, collapseRawFixedWordSummand mu r z lstar ↑d = ∑ shape ∈ activeCollapseShapes mu r M, ∑ d ∈ specFixedRawCollapseData (splitLeafMultiplicity mu r) M with (↑d).collapseShape = shape, collapseRawFixedWordSummand mu r z lstar ↑d

The raw fixed-word total is exactly the sum over occurring shapes with at least two blocks; all other shape fibers vanish by primitivity.