The permutation-sum estimate #
Run compression reduces Proposition 5.7 to Proposition 5.9. The source
sum is regrouped first by compressed word and then by compressed
multiplicity profile. The two finite ledgers cost 4^(2n), the
factorial comparison costs 4^n, and the resulting 64^n is absorbed
into one absolute constant.
theorem
Anderson4D.paperSum_primitiveChainWeight_eq_primitiveMergeWordFamily
{t : PlaneTree}
{M : ℕ}
(mu : t.Multiplicities)
(z : HeppLeaf t → Fin 4 → ℤ)
:
paperSum (leafMultiplicity mu) (primitiveChainWeight z) = ∑ w ∈ primitiveMergeWordFamily (leafMultiplicity mu),
(∏ l : HeppLeaf t, ↑(leafMultiplicity mu l).factorial) * heppChainWeight z (listWord (mergedProfileOutcome (leafMultiplicity mu) w).2)
The exact P-5.7 paperSum is the primitive valid-word family used by
the run-compression regrouping, with the original factorial ledger kept
outside each compressed chain weight.
theorem
Anderson4D.primitiveProfileFiber_le_uniformTarget
{C0 D : ℝ}
(hinductive : InductiveEstimate C0 D)
{t : PlaneTree}
{R n : ℕ}
(ht : t.isValid = true)
(hroot : t.rootV ∈ t.BranchNodes)
(Nm : t.HeppMarking)
(mu : t.Multiplicities)
(z : HeppLeaf t → Fin 4 → ℤ)
(hadmissible : IsAdmissible Nm R z)
(htotal : totalMultiplicity mu = 2 * n)
(p : MergeMultiplicityProfile (leafMultiplicity mu))
(hp : p ∈ mergeMultiplicityProfileImage (leafMultiplicity mu) (primitiveMergeWordFamily (leafMultiplicity mu)))
:
∑ q ∈ mergeProfileOutcomeImage (leafMultiplicity mu) (primitiveMergeWordFamily (leafMultiplicity mu)) with q.1 = p,
(∏ l : HeppLeaf t, ↑(leafMultiplicity mu l).factorial) * heppChainWeight z (listWord q.2) ≤ C0 ^ (2 * n) * D ^ t.BranchNodes.card * 4 ^ n * ∑ W ∈ (nonrootBranches t).powerset, permSumSummand n Nm mu W
One realized compressed profile is controlled uniformly by the P-5.9 estimate and the factorial comparison.