Raw-collapse finite-sum bound

This module combines the exact raw-data reindexing of the P-5.9 paper sum with the fixed-word (5.43) estimate. The named summands below expose the finite family that the subsequent Fubini regrouping consumes.

Named raw-data summands

noncomputable def Anderson4D.collapseRawLedgerCoefficient {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : ℝ

Factorial coefficient attached to a raw collapse datum by the exact marker-fiber ledger.

Equations

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

theorem Anderson4D.collapseRawLedgerCoefficient_nonneg {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : 0 ≤ collapseRawLedgerCoefficient mu r d

The factorial ledger is nonnegative, as required to multiply a pointwise chain-weight inequality.

noncomputable def Anderson4D.collapseRawReindexedSummand {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : ℝ

Named summand in the exact raw-data reindexing, before applying (5.43).

Equations

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

noncomputable def Anderson4D.collapseRawFixedWordSummand {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : ℝ

Explicit active fixed-word summand prepared for Fubini regrouping. Its indicator displays all three conditions that make the raw contribution nonzero and admissible for the two recursive subproblems.

Equations

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

Exact reindexed sum

theorem Anderson4D.paperSum_primitiveSeparated_eq_sum_collapseRawReindexedSummand {t : PlaneTree} {M : ℕ} (mu : t.Multiplicities) (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) = ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M, collapseRawReindexedSummand mu r z ↑d

The exact P-5.9 collapse reindexing expressed using the named raw summand.

Pointwise and finite-sum bounds

theorem Anderson4D.collapseRawReindexedSummand_le_fixedWordSummand {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) : collapseRawReindexedSummand mu r z d ≤ collapseRawFixedWordSummand mu r z lstar d

Every reindexed raw summand is bounded by its explicit active fixed-word summand. Inactive data vanish on both sides; in the active case the nonnegative factorial coefficient multiplies the fixed-word (5.43) estimate.

theorem Anderson4D.paperSum_primitiveSeparated_le_sum_collapseRawFixedWord {t : PlaneTree} {M : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (_compound : Finset t.VPos) (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) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) ≤ ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M, collapseRawFixedWordSummand mu r z lstar ↑d

Tree-facing raw-data finite-sum upper bound. The compound argument is carried explicitly for the subsequent collapse assembly, although this chain-only stage does not inspect it.

theorem Anderson4D.paperSum_primitiveSeparated_le_sum_collapseRawFixedWord_explicit {t : PlaneTree} {M : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (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) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) ≤ ∑ d : FixedRawCollapseData (InsideLeaf r) (OutsideLeaf r) M, if CollapseMultiplicitySpec (splitLeafMultiplicity mu r) ↑d ∧ NoProperLeafBlock (↑d).expandedWord ∧ NoAdjacentEqual (↑d).expandedWord then collapseRawLedgerCoefficient mu r ↑d * 4 ^ (↑d).insideLength * singleScaleChainWeight (restrictEmbedding z r) (↑d).adjacentCutIndices (restrictedInsideWord r ↑d) * primitiveSeparatedChainWeight (contractEmbedding z r lstar) (contractedCollapsedWord r ↑d) else 0

Fully expanded form of the raw-data bound, matching the summand that is regrouped in the next Fubini step.