Fixed-shape regrouping of the raw collapse sum

On one fixed block-composition shape, the raw datum is injectively determined by its flattened inside list and collapsed list. This module separates the fixed-word majorant into a nonnegative weight of each list and applies the finite Fubini bound. No estimate for the number of shapes is taken here.

The cut set determined by a shape

noncomputable def Anderson4D.collapseShapeAdjacentCutIndices (shape : List ℕ) (n : ℕ) : Finset (AdjacentIndex n)

Proper partial sums of shape, represented as adjacency indices of an arbitrary list. The definition remains total when the list has the wrong length; the fixed-shape application only uses the matching length.

Equations

• Anderson4D.collapseShapeAdjacentCutIndices shape n = {j : Anderson4D.AdjacentIndex n | ∃ (i : ℕ), i + 1 < shape.length ∧ (List.take (i + 1) shape).sum = ↑↑j + 1}

@[simp]

theorem Anderson4D.mem_collapseShapeAdjacentCutIndices_iff (shape : List ℕ) (n : ℕ) (j : AdjacentIndex n) : j ∈ collapseShapeAdjacentCutIndices shape n ↔ ∃ (i : ℕ), i + 1 < shape.length ∧ (List.take (i + 1) shape).sum = ↑↑j + 1

theorem Anderson4D.RawCollapseData.adjacentCutIndices_eq_shape {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) (shape : List ℕ) (hshape : d.collapseShape = shape) : d.adjacentCutIndices = collapseShapeAdjacentCutIndices shape d.insideLength

A raw datum in the shape fiber has exactly the shape-defined cut set.

Word and list chain weights

noncomputable def Anderson4D.collapseInsideWordChainWeight {A : Type u_1} [DecidableEq A] {n : ℕ} (z : A → Fin 4 → ℤ) (shape : List ℕ) (w : Fin n → A) : ℝ

P-5.10's cut-exception summand with the cut set determined by shape.

Equations

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

noncomputable def Anderson4D.collapseInsideListChainWeight {A : Type u_1} [DecidableEq A] (z : A → Fin 4 → ℤ) (shape : List ℕ) (l : List A) : ℝ

The same weight as a function of the underlying list, for fixed-shape Fubini separation.

Equations

• Anderson4D.collapseInsideListChainWeight z shape l = Anderson4D.collapseInsideWordChainWeight z shape (Anderson4D.listWord l)

def Anderson4D.castFinWord {A : Type u_1} {n m : ℕ} (h : n = m) (w : Fin n → A) : Fin m → A

Transport a finite word across an equality of its carrier lengths.

Equations

• Anderson4D.castFinWord h w i = w (Fin.cast ⋯ i)

@[simp]

theorem Anderson4D.castFinWord_listWord_ofFn {A : Type u_1} {n : ℕ} (w : Fin n → A) : castFinWord ⋯ (listWord (List.ofFn w)) = w

theorem Anderson4D.collapseInsideWordChainWeight_cast {A : Type u_1} [DecidableEq A] {n m : ℕ} (z : A → Fin 4 → ℤ) (shape : List ℕ) (h : n = m) (w : Fin n → A) : collapseInsideWordChainWeight z shape w = collapseInsideWordChainWeight z shape (castFinWord h w)

The inside chain statistic is invariant under transport of the finite carrier along a length equality.

theorem Anderson4D.collapseInsideWordChainWeight_nonneg {A : Type u_1} [DecidableEq A] {n : ℕ} (z : A → Fin 4 → ℤ) (shape : List ℕ) (w : Fin n → A) : 0 ≤ collapseInsideWordChainWeight z shape w

theorem Anderson4D.collapseInsideListChainWeight_nonneg {A : Type u_1} [DecidableEq A] (z : A → Fin 4 → ℤ) (shape : List ℕ) (l : List A) : 0 ≤ collapseInsideListChainWeight z shape l

@[simp]

theorem Anderson4D.collapseInsideListChainWeight_ofFn {A : Type u_1} [DecidableEq A] {n : ℕ} (z : A → Fin 4 → ℤ) (shape : List ℕ) (w : Fin n → A) : collapseInsideListChainWeight z shape (List.ofFn w) = collapseInsideWordChainWeight z shape w

theorem Anderson4D.collapseInsideWordChainWeight_eq_restricted {t : PlaneTree} {n : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) (w : Fin n → InsideLeaf r) : collapseInsideWordChainWeight (fun (a : InsideLeaf r) => z ↑a) shape w = singleScaleChainWeight (restrictEmbedding z r) (collapseShapeAdjacentCutIndices shape n) ((wordRenameEquiv (restrictInsideAlphabetEquiv r) n) w)

Renaming a fixed-shape inside word to the restricted-tree alphabet turns the raw shape weight into the exact P-5.10 summand.

theorem Anderson4D.RawCollapseData.blocks_length_eq_shape_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) {shape : List ℕ} (hshape : d.collapseShape = shape) : d.blocks.length = shape.length

Shape length is the number of blocks in every datum of the fiber.

theorem Anderson4D.RawCollapseData.insideLength_eq_shape_sum {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) {shape : List ℕ} (hshape : d.collapseShape = shape) : d.insideLength = shape.sum

Shape mass is the flattened inside length in every datum of the fiber.

theorem Anderson4D.RawCollapseData.collapseInsideListChainWeight_eq_singleScale {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (shape : List ℕ) (hshape : d.collapseShape = shape) : collapseInsideListChainWeight (fun (a : InsideLeaf r) => z ↑a) shape d.insideList = singleScaleChainWeight (restrictEmbedding z r) d.adjacentCutIndices (restrictedInsideWord r d)

The list-only inside chain is exactly the actual restricted-tree single-scale summand on a datum in the shape fiber.

Fixed-shape marginal weights

noncomputable def Anderson4D.collapseInsideShapeWeight {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) (l : List (InsideLeaf r)) : ℝ

Inside-list marginal: inverse marker factorial, inside factorial ledger, the geometric 4^n, and the restricted single-scale word weight.

Equations

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

noncomputable def Anderson4D.collapseContractedShapeWeight {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (shape : List ℕ) (l : List (Unit ⊕ OutsideLeaf r)) : ℝ

Collapsed-list marginal: contracted factorial ledger and the raw marker/outside primitive-separated word weight.

Equations

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

theorem Anderson4D.collapseInsideShapeWeight_nonneg {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) (l : List (InsideLeaf r)) : 0 ≤ collapseInsideShapeWeight mu z r shape l

theorem Anderson4D.collapseContractedShapeWeight_nonneg {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (shape : List ℕ) (l : List (Unit ⊕ OutsideLeaf r)) : 0 ≤ collapseContractedShapeWeight mu z r lstar shape l

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_cast {A : Type u_1} [Fintype A] [DecidableEq A] {n m : ℕ} (z : A → Fin 4 → ℤ) (h : n = m) (w : Fin n → A) : primitiveSeparatedAlphabetChainWeight z w = primitiveSeparatedAlphabetChainWeight z (castFinWord h w)

The primitive-separated alphabet statistic is invariant under transport of the finite carrier along a length equality.

@[simp]

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_listWord_ofFn {A : Type u_1} [Fintype A] [DecidableEq A] {n : ℕ} (z : A → Fin 4 → ℤ) (w : Fin n → A) : primitiveSeparatedAlphabetChainWeight z (listWord (List.ofFn w)) = primitiveSeparatedAlphabetChainWeight z w

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_eq_contracted {t : PlaneTree} {n : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (w : Fin n → Unit ⊕ OutsideLeaf r) : primitiveSeparatedAlphabetChainWeight (collapsedCollapsePoint z r lstar) w = primitiveSeparatedChainWeight (contractEmbedding z r lstar) ((wordRenameEquiv (contractCollapsedAlphabetEquiv r) n) w)

Renaming a marker/outside word to the contracted-tree alphabet turns the raw alphabet statistic into the exact contracted P-5.9 summand.

Exact factorization on a shape fiber

theorem Anderson4D.RawCollapseData.collapseContractedListChainWeight_eq {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : primitiveSeparatedAlphabetChainWeight (collapsedCollapsePoint z r lstar) (listWord d.collapsed) = primitiveSeparatedChainWeight (contractEmbedding z r lstar) (contractedCollapsedWord r d)

The raw collapsed-list statistic is the primitive-separated statistic of the corresponding word on the contracted tree.

theorem Anderson4D.collapseRawFixedWordSummand_eq_shapeWeights_of_active {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (shape : List ℕ) (hshape : d.collapseShape = shape) (hactive : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d ∧ NoProperLeafBlock d.expandedWord ∧ NoAdjacentEqual d.expandedWord) : collapseRawFixedWordSummand mu r z lstar d = collapseInsideShapeWeight mu z r shape d.insideList * collapseContractedShapeWeight mu z r lstar shape d.collapsed

On an active datum in a fixed shape fiber, every factor in the raw majorant splits exactly into an inside-list and a collapsed-list marginal.

theorem Anderson4D.collapseRawFixedWordSummand_le_shapeWeights {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (shape : List ℕ) (hshape : d.collapseShape = shape) : collapseRawFixedWordSummand mu r z lstar d ≤ collapseInsideShapeWeight mu z r shape d.insideList * collapseContractedShapeWeight mu z r lstar shape d.collapsed

The factorized nonnegative marginals dominate the raw summand on every datum in the shape fiber, including inactive data.

Valid-word coordinates on a spec shape fiber

@[reducible, inline]

abbrev Anderson4D.SpecFixedRawCollapseShapeData {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (M : ℕ) (shape : List ℕ) : Type

Fixed-shape data that also satisfy the prescribed split multiplicity.

Equations

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

def Anderson4D.SpecFixedRawCollapseShapeData.toFixedShape {t : PlaneTree} {mu : t.Multiplicities} {r : t.VPos} {M : ℕ} {shape : List ℕ} (d : SpecFixedRawCollapseShapeData mu r M shape) : FixedRawCollapseShapeData (InsideLeaf r) (OutsideLeaf r) M shape

Forget only the multiplicity certificate, retaining the fixed-shape certificate.

Equations

• d.toFixedShape = ⟨↑d, ⋯⟩

theorem Anderson4D.castFinWord_mem_validWords_iff {A : Type u_1} [Fintype A] [DecidableEq A] {n m : ℕ} (h : n = m) (mult : A → ℕ) (w : Fin n → A) : castFinWord h w ∈ validWords mult ↔ w ∈ validWords mult

theorem Anderson4D.fixedShapeInsideWord_mem_validWords_of_spec {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {M : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B M shape) (hSpec : CollapseMultiplicitySpec mult ↑↑d) : fixedShapeInsideWord d ∈ validWords (insideMultiplicity mult)

The fixed-shape inside coordinate has exactly the prescribed raw inside multiplicity.

theorem Anderson4D.fixedShapeCollapsedWord_mem_validWords_of_spec {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {M : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B M shape) (hSpec : CollapseMultiplicitySpec mult ↑↑d) : fixedShapeCollapsedWord d ∈ validWords (markerMultiplicity shape.length (outsideMultiplicity mult))

The fixed-shape collapsed coordinate has the marker multiplicity shape.length and the prescribed outside multiplicities.

Tree-facing valid-word subtypes

@[reducible, inline]

abbrev Anderson4D.RestrictedShapeValidWord {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (shape : List ℕ) : Type

Valid restricted-tree words on the fixed inside length.

Equations

• Anderson4D.RestrictedShapeValidWord mu r shape = ↥(Anderson4D.validWords (Anderson4D.leafMultiplicity (Anderson4D.restrictMultiplicities mu r)))

@[reducible, inline]

abbrev Anderson4D.ContractedShapeValidWord {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : Type

Valid contracted-tree words on the fixed collapsed length.

Equations

• Anderson4D.ContractedShapeValidWord mu r M shape hs = ↥(Anderson4D.validWords (Anderson4D.leafMultiplicity (Anderson4D.contractMultiplicities mu r (shape.length - 1) hs)))

theorem Anderson4D.fixedShapeContractedMultiplicity_eq {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : renameMultiplicity (contractCollapsedAlphabetEquiv r) (markerMultiplicity shape.length (outsideMultiplicity (splitLeafMultiplicity mu r))) = leafMultiplicity (contractMultiplicities mu r (shape.length - 1) hs)

At fixed shape, the renamed marker/outside multiplicity is exactly the leaf multiplicity of the one contracted tree used by the induction call.

def Anderson4D.specShapeRestrictedValidWord {t : PlaneTree} {mu : t.Multiplicities} {r : t.VPos} {M : ℕ} {shape : List ℕ} (d : SpecFixedRawCollapseShapeData mu r M shape) : RestrictedShapeValidWord mu r shape

The inside coordinate of a spec+shape datum, packaged directly as a valid word for the restricted-tree paperSum.

Equations

• Anderson4D.specShapeRestrictedValidWord d = ⟨(Anderson4D.wordRenameEquiv (Anderson4D.restrictInsideAlphabetEquiv r) shape.sum) (Anderson4D.fixedShapeInsideWord d.toFixedShape), ⋯⟩

def Anderson4D.specShapeContractedValidWord {t : PlaneTree} {mu : t.Multiplicities} {r : t.VPos} {M : ℕ} {shape : List ℕ} (hs : 1 ≤ shape.length - 1) (d : SpecFixedRawCollapseShapeData mu r M shape) : ContractedShapeValidWord mu r M shape hs

The collapsed coordinate of a spec+shape datum, packaged directly as a valid word for the fixed contracted-tree paperSum.

Equations

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

theorem Anderson4D.specShapeValidWordPair_injective {t : PlaneTree} {mu : t.Multiplicities} {r : t.VPos} {M : ℕ} {shape : List ℕ} (hs : 1 ≤ shape.length - 1) : Function.Injective fun (d : SpecFixedRawCollapseShapeData mu r M shape) => (specShapeRestrictedValidWord d, specShapeContractedValidWord hs d)

No multiplicity-bearing raw datum is counted twice by the two tree-facing valid-word coordinates.

Valid-word marginal weights

noncomputable def Anderson4D.restrictedShapeMarginalWeight {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) (w : RestrictedShapeValidWord mu r shape) : ℝ

Inside marginal on exactly the valid restricted-tree words.

Equations

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

noncomputable def Anderson4D.contractedShapeMarginalWeight {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) (w : ContractedShapeValidWord mu r M shape hs) : ℝ

Collapsed marginal on exactly the valid contracted-tree words.

Equations

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

theorem Anderson4D.restrictedShapeMarginalWeight_nonneg {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) (w : RestrictedShapeValidWord mu r shape) : 0 ≤ restrictedShapeMarginalWeight mu z r shape w

theorem Anderson4D.contractedShapeMarginalWeight_nonneg {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) (w : ContractedShapeValidWord mu r M shape hs) : 0 ≤ contractedShapeMarginalWeight mu z r lstar M shape hs w

theorem Anderson4D.collapseInsideShapeWeight_eq_restrictedMarginal {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) {M : ℕ} {shape : List ℕ} (d : SpecFixedRawCollapseShapeData mu r M shape) : collapseInsideShapeWeight mu z r shape (↑↑d).insideList = restrictedShapeMarginalWeight mu z r shape (specShapeRestrictedValidWord d)

On a spec+shape coordinate, the list-level inside marginal is exactly the corresponding restricted valid-word marginal.

theorem Anderson4D.collapseContractedShapeWeight_eq_contractedMarginal {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) {M : ℕ} {shape : List ℕ} (hs : 1 ≤ shape.length - 1) (d : SpecFixedRawCollapseShapeData mu r M shape) : collapseContractedShapeWeight mu z r lstar shape (↑↑d).collapsed = contractedShapeMarginalWeight mu z r lstar M shape hs (specShapeContractedValidWord hs d)

On a spec+shape coordinate, the list-level collapsed marginal is exactly the corresponding contracted valid-word marginal.

Exact marginal sums

theorem Anderson4D.sum_validWordSubtype_eq_wordSum {A : Type u_1} [Fintype A] [DecidableEq A] {n : ℕ} (mult : A → ℕ) (F : (Fin n → A) → ℝ) : ∑ w : ↥(validWords mult), F ↑w = wordSum mult F

Summing over the subtype attached to validWords is exactly wordSum; no unrestricted word family is introduced.

theorem Anderson4D.sum_restrictedShapeMarginalWeight_eq_paperSum {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (shape : List ℕ) : ∑ w : RestrictedShapeValidWord mu r shape, restrictedShapeMarginalWeight mu z r shape w = (↑shape.length.factorial)⁻¹ * 4 ^ shape.sum * paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) (collapseShapeAdjacentCutIndices shape shape.sum))

The restricted valid-word marginal sums to the inverse marker factorial and geometric factor times the exact restricted paperSum.

theorem Anderson4D.sum_contractedShapeMarginalWeight_eq_paperSum {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : ∑ w : ContractedShapeValidWord mu r M shape hs, contractedShapeMarginalWeight mu z r lstar M shape hs w = paperSum (leafMultiplicity (contractMultiplicities mu r (shape.length - 1) hs)) (primitiveSeparatedChainWeight (contractEmbedding z r lstar))

The contracted valid-word marginal sums to the exact contracted-tree paperSum, including its full factorial ledger.

Concrete fixed-shape Fubini bound

theorem Anderson4D.sum_specShape_shapeWeights_le_validMarginalProduct {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : ∑ d : SpecFixedRawCollapseShapeData mu r M shape, collapseInsideShapeWeight mu z r shape (↑↑d).insideList * collapseContractedShapeWeight mu z r lstar shape (↑↑d).collapsed ≤ (∑ w : RestrictedShapeValidWord mu r shape, restrictedShapeMarginalWeight mu z r shape w) * ∑ w : ContractedShapeValidWord mu r M shape hs, contractedShapeMarginalWeight mu z r lstar M shape hs w

The exact valid-word Fubini step for the two factorized marginals. Both target types are attached to validWords; no sum over all words appears.

theorem Anderson4D.sum_specShape_collapseRawFixedWordSummand_le_paperSums {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : ∑ d : SpecFixedRawCollapseShapeData mu r M shape, collapseRawFixedWordSummand mu r z lstar ↑↑d ≤ (↑shape.length.factorial)⁻¹ * 4 ^ shape.sum * paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) (collapseShapeAdjacentCutIndices shape shape.sum)) * paperSum (leafMultiplicity (contractMultiplicities mu r (shape.length - 1) hs)) (primitiveSeparatedChainWeight (contractEmbedding z r lstar))

Concrete P-5.9 fixed-shape Fubini bound: the raw fixed-word majorant is bounded by exactly the two paper sums, with the inverse marker factorial and 4^n allocated once.

theorem Anderson4D.sum_specFixedRawCollapseShapeData_eq_filter {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (M : ℕ) (shape : List ℕ) (F : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M → ℝ) : ∑ d : SpecFixedRawCollapseShapeData mu r M shape, F ↑d = ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M with CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d ∧ (↑d).collapseShape = shape, F d

A subtype sum over the spec+shape source is the corresponding filtered sum over fixed-length raw data.

theorem Anderson4D.sum_filter_specShape_collapseRawFixedWordSummand_le_paperSums {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (shape : List ℕ) (hs : 1 ≤ shape.length - 1) : ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M with CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d ∧ (↑d).collapseShape = shape, collapseRawFixedWordSummand mu r z lstar ↑d ≤ (↑shape.length.factorial)⁻¹ * 4 ^ shape.sum * paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) (collapseShapeAdjacentCutIndices shape shape.sum)) * paperSum (leafMultiplicity (contractMultiplicities mu r (shape.length - 1) hs)) (primitiveSeparatedChainWeight (contractEmbedding z r lstar))

Filtered fixed-length form of the concrete valid-word Fubini bound.

Witness-facing transport

theorem Anderson4D.collapseShapeAdjacentCutIndices_heq (shape : List ℕ) {n m : ℕ} (h : n = m) : collapseShapeAdjacentCutIndices shape n ≍ collapseShapeAdjacentCutIndices shape m

Shape cut sets at propositionally equal lengths are heterogeneously equal.

theorem Anderson4D.paperSum_singleScale_eq_of_length_and_cuts {t : PlaneTree} {n m : ℕ} (mult : HeppLeaf t → ℕ) (z : HeppLeaf t → Fin 4 → ℤ) (O₁ : Finset (AdjacentIndex n)) (O₂ : Finset (AdjacentIndex m)) (hlength : n = m) (hcuts : O₁ ≍ O₂) : paperSum mult (singleScaleChainWeight z O₁) = paperSum mult (singleScaleChainWeight z O₂)

A single-scale paperSum is unchanged when its word length and cut set are transported together.

theorem Anderson4D.paperSum_primitiveSeparated_eq_of_length_and_multiplicity {t : PlaneTree} {n m : ℕ} {mult₁ mult₂ : HeppLeaf t → ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (hlength : n = m) (hmult : mult₁ = mult₂) : paperSum mult₁ (primitiveSeparatedChainWeight z) = paperSum mult₂ (primitiveSeparatedChainWeight z)

A primitive-separated paperSum is unchanged when both its word length and prescribed multiplicity are transported.

theorem Anderson4D.contractMultiplicities_eq_of_cutCount_eq {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) {s₁ s₂ : ℕ} (h : s₁ = s₂) (hs₁ : 1 ≤ s₁) (hs₂ : 1 ≤ s₂) : contractMultiplicities mu r s₁ hs₁ = contractMultiplicities mu r s₂ hs₂

The proof argument in contractMultiplicities is irrelevant when the cut counts are propositionally equal.

theorem Anderson4D.sum_filter_witnessShape_collapseRawFixedWordSummand_le_paperSums {t : PlaneTree} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (M : ℕ) (d₀ : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M) (_hSpec₀ : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d₀) (hblocks : 2 ≤ (↑d₀).blocks.length) : ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M with CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d ∧ (↑d).collapseShape = (↑d₀).collapseShape, collapseRawFixedWordSummand mu r z lstar ↑d ≤ 4 ^ (↑d₀).insideLength * (↑(collapseCutCount ↑d₀ + 1).factorial)⁻¹ * paperSum (leafMultiplicity (restrictMultiplicities mu r)) (singleScaleChainWeight (restrictEmbedding z r) (↑d₀).adjacentCutIndices) * paperSum (leafMultiplicity (contractMultiplicities mu r (collapseCutCount ↑d₀) ⋯)) (primitiveSeparatedChainWeight (contractEmbedding z r lstar))

Witness-facing form of the fixed-shape bound. Its right side has exactly the product consumed by collapse_analytic_product...: the witness's actual cut set, cut count, and collapsed length.