Global assembly of the outer single-scale majority estimate

This file performs only the finite outer assembly which follows the fixed-P estimate (5.82)--(5.86). The active P classes partition the Hepp leaves exactly, so the fixed-fiber bounds multiply without duplicating any leaf payoff and their exponential losses add to the total multiplicity.

The P-word sequence gain and the final Fubini/reordering step of Proposition 5.10 belong to later files.

def Anderson4D.leafPClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (l : HeppLeaf t) : ℕ

The unique P = YN⁴ class attached to a Hepp leaf.

Equations

• Anderson4D.leafPClass Nm mu l = Anderson4D.singleScaleSigma3 (Anderson4D.singleScaleSigma2 Nm mu (Anderson4D.singleScaleSigma1 Nm mu l))

theorem Anderson4D.leafPClass_mem_pCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (l : HeppLeaf t) : leafPClass Nm mu l ∈ pCarrier Nm mu

theorem Anderson4D.mem_leavesAtP_iff_leafPClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) (l : HeppLeaf t) : l ∈ leavesAtP Nm mu P ↔ leafPClass Nm mu l = P

theorem Anderson4D.leavesAtP_pairwiseDisjoint {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : (↑(pCarrier Nm mu)).PairwiseDisjoint (leavesAtP Nm mu)

Distinct active P classes have disjoint exact leaf fibers.

theorem Anderson4D.biUnion_leavesAtP_eq_univ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : (pCarrier Nm mu).biUnion (leavesAtP Nm mu) = Finset.univ

The active P fibers cover every Hepp leaf, with no off-carrier residue.

theorem Anderson4D.sum_multiplicityP_eq_totalMultiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ∑ P ∈ pCarrier Nm mu, multiplicityP Nm mu P = totalMultiplicity mu

The full multiplicity ledger is the sum of the exact P-fiber ledgers.

theorem Anderson4D.leavesAtP_product_eq_global {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (f : HeppLeaf t → ℝ) : ∏ P ∈ pCarrier Nm mu, ∏ l ∈ leavesAtP Nm mu P, f l = ∏ l : HeppLeaf t, f l

Products over the exact P fibers flatten to one global leaf product. This is the product-level form of both disjointness and coverage.

theorem Anderson4D.fixedP_outerMultinomial_le_originalPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ), ↑(Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)) ≤ C ^ multiplicityP Nm mu P * ∏ l ∈ leavesAtP Nm mu P, originalOuterLeafPayoff Nm mu compound l

The complete fixed-P outer refinement: first pass from the (N,X) multinomial to the outer (N,Y) multinomial, then apply the majority estimate (5.82)--(5.86). The two uniform exponential constants are merged.

theorem Anderson4D.globalOuterMajorityRefinement : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree}, t.isValid = true → t.rootV ∈ t.BranchNodes → ∀ (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos), ∏ P ∈ pCarrier Nm mu, ↑(Nat.multinomial (nxAtP Nm mu P) (multiplicityNX Nm mu)) ≤ C ^ totalMultiplicity mu * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l

Global outer refinement bound obtained by multiplying the completed fixed-P majority estimate over pCarrier. The constant is uniform, its exponent is exactly the total word length, and every original leaf payoff occurs exactly once.