Outer aggregation for a fixed coarse class word

This file combines three finite ledgers used after the fixed-(N,X) inner estimate:

• the number of valid (N,X) refinements of a fixed active-P word;
• the anchor-dependent oriented active-P sequence weight;
• the global simple/compound majority payoff.

The positional exceptional set is independent of the analytic class word. Consequently, an anchor selected separately for every refinement can first be enlarged to the sum over every anchor and every active-P word. The remaining refinement cardinal is exactly paper (5.79).

theorem Anderson4D.XYCluster.anchoredOrientedActivePWeight_nonneg (theta : ℝ) {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {n : ℕ} (E : Finset (Fin n)) (anchor : Fin (n + 1)) (w : Fin (n + 1) → ActivePClass Nm mu) : 0 ≤ anchoredOrientedActivePWeight theta E anchor w

Every original-edge active-P weight is nonnegative.

theorem Anderson4D.XYCluster.sum_anchorSelected_orientedActivePWeight_le (theta : ℝ) {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {n : ℕ} (s : Finset (Fin (n + 1) → ActiveNXClass Nm mu)) (chooseAnchor : (Fin (n + 1) → ActiveNXClass Nm mu) → Fin (n + 1)) (E : Fin (n + 1) → Finset (Fin n)) : (∑ x ∈ s, anchoredOrientedActivePWeight theta (E (chooseAnchor x)) (chooseAnchor x) fun (i : Fin (n + 1)) => activeNXToP Nm mu (x i)) ≤ ↑s.card * ∑ anchor : Fin (n + 1), ∑ w : Fin (n + 1) → ActivePClass Nm mu, anchoredOrientedActivePWeight theta (E anchor) anchor w

An arbitrary anchor choice for every member of a finite family costs no more than the family cardinal times the sum over all anchors and all words. This is the abstract enlargement used before applying the sequence theorem.

theorem Anderson4D.XYCluster.paper579_conditional_classWord_count_of_length {t : PlaneTree} {M : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (y : Fin M → ActivePClass Nm mu) (hy : y ∈ validWords (activePMultiplicity Nm mu)) : (validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y).card = ∏ P ∈ pCarrier Nm mu, Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)

Length-polymorphic form of paper (5.79). The paper-facing theorem fixes the domain to Fin (totalMultiplicity mu); this form is convenient after writing that length syntactically as (totalMultiplicity mu - 1) + 1.

theorem Anderson4D.XYCluster.fixedPWord_refinement_orientedWeight_le_originalPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos), have n := totalMultiplicity mu - 1; ∀ y ∈ validWords (activePMultiplicity Nm mu), ∀ (chooseAnchor : (Fin (n + 1) → ActiveNXClass Nm mu) → Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))), (∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, anchoredOrientedActivePWeight (1 / 16) (finAnchorPositionalInterpolatedExceptionalFinEdges false false (chooseAnchor x) O) (chooseAnchor x) fun (i : Fin (n + 1)) => activeNXToP Nm mu (x i)) ≤ C ^ totalMultiplicity mu * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l

Outer aggregation for one valid active-P word.

Each valid (N,X) refinement may choose its own anchor. Both phase flags are fixed to false; the interpolated exceptional set is the purely positional one, hence independent of the refinement word. The resulting weighted refinement sum is bounded by one exponential constant times the global original outer-leaf payoff.

theorem Anderson4D.XYCluster.global_refinement_orientedWeight_le_originalPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos), have n := totalMultiplicity mu - 1; ∀ (chooseAnchor : (Fin (n + 1) → ActiveNXClass Nm mu) → Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))), (∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, anchoredOrientedActivePWeight (1 / 16) (finAnchorPositionalInterpolatedExceptionalFinEdges false false (chooseAnchor x) O) (chooseAnchor x) fun (i : Fin (n + 1)) => activeNXToP Nm mu (x i)) ≤ C ^ totalMultiplicity mu * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l

Global outer ledger consumed by the final single-scale assembly.

The sum is first over every valid active-P word and then over all valid (N,X) refinements. The refinement condition identifies the active-P word of each fine word with the fixed outer word. Since the refinement cardinality is independent of that outer word, paper (5.79) can be pulled out before the valid-word carrier is enlarged to all active-P functions. The sequence estimate is therefore used exactly once.

theorem Anderson4D.XYCluster.global_refinement_common_mul_orientedWeight_le_originalPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos), have n := totalMultiplicity mu - 1; ∀ (chooseAnchor : (Fin (n + 1) → ActiveNXClass Nm mu) → Fin (n + 1)) (O : Finset (AdjacentIndex (n + 1))) (common : ℝ), 0 ≤ common → (∑ y ∈ validWords (activePMultiplicity Nm mu), ∑ x ∈ validRefinements (activeNXMultiplicity Nm mu) (activeNXToP Nm mu) y, common * anchoredOrientedActivePWeight (1 / 16) (finAnchorPositionalInterpolatedExceptionalFinEdges false false (chooseAnchor x) O) (chooseAnchor x) fun (i : Fin (n + 1)) => activeNXToP Nm mu (x i)) ≤ (C ^ totalMultiplicity mu * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l) * common

The global outer ledger with an arbitrary nonnegative coefficient common to every fine word. This form preserves the word-independent completed base-scale coefficient supplied by SingleScaleAnchorScaleLedger.