Analytic bound for one collapse-shape fiber

This module joins the validity-preserving fixed-shape Fubini bound to the two analytic calls in the eligible-collapse step. The witness datum fixes the actual cut set, cut count, inside length, and contracted word length used by both sides of the estimate.

theorem Anderson4D.sum_filter_witnessShape_collapseRawFixedWordSummand_le_sum_combinedCollapseTerm {C0 D : ℝ} (hsingle : SingleScaleEstimate C0) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (hcompound : compound ⊆ t.Leaves) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : IsLowestCollapseEligible Nm mu r) (lstar : InsideLeaf r) {M : ℕ} (d₀ : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M) (hSpec₀ : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d₀) (hblocks : 2 ≤ (↑d₀).blocks.length) (hIH : InductiveConclusion C0 D (t.contractAt ↑r)) : ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M with CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d ∧ (↑d).collapseShape = (↑d₀).collapseShape, collapseRawFixedWordSummand mu r z lstar ↑d ≤ ∑ W ∈ (nonrootBranches (t.contractAt ↑r)).powerset, combinedCollapseTerm C0 D (↑d₀).insideLength (collapseCutCount ↑d₀) (↑d₀).collapsed.length Nm mu compound r ⋯ W

A single multiplicity-valid collapse-shape fiber is bounded by the contracted-tree W-sum of combinedCollapseTerm.

The first inequality is the concrete valid-word Fubini regrouping; the second is exactly the product of Proposition 5.10 on the restricted tree and the P-5.9 induction hypothesis on the contracted tree.