The simple/compound majority split in the outer single-scale sum

This file formalizes the part of Step 3 of Proposition 5.10 which starts at paper (5.82). The classification is made on the canonical maximal-X fiber of every active (N,Y) class, namely maxNXAtNY; it is not made on the whole (N,Y) fiber.

There is a small but essential normalization hidden in the prose following (5.82). The simple estimate (5.83) uses m_l > 2, although Proposition 5.10 only assumes m_l ≥ 2. We therefore declare every simple leaf of multiplicity two compound for this local classification. The tie rule is:

• a tie is assigned to the simple class;
• otherwise the strict majority decides.

The relabeling is harmless only at exponential cost: a relabeled leaf replaces the simple factor N^(2(m_l-2)) = 1 by (2!)^(1/4) ≤ 2. The theorem normalizedMajorityPayoff_le records this cost explicitly.

The principal results below are:

• fixedP_majority_partition_le, the actual fixed-P specialization of (5.82);
• simpleMajority_exponent_payoff, a denominator-free form of (5.83);
• simpleMajority_multinomial_le_ordered, the exact (5.84) inequality once the simple classes have been enumerated in increasing scale order;
• compoundMajority_factorial_certificate, an eighth-power, integral form of (5.85), with an explicit exponential loss;
• fixedP_majority_multinomial_le_originalPayoff, the complete fixed-P assembly of (5.82)--(5.86), including disjoint canonical-fiber flattening and the multiplicity-two normalization.

The canonical maximal fiber and the normalized leaf types

noncomputable def Anderson4D.maxFiberAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : Finset (HeppLeaf t)

The paper's set L_{N,X*} for an (N,Y) class. It is empty off the active carrier, which makes the definition total without adding a proof argument to all later finite sets.

Equations

• Anderson4D.maxFiberAtNY Nm mu q = if hq : q ∈ Anderson4D.nyCarrier Nm mu then Anderson4D.leavesAtNX Nm mu (Anderson4D.maxNXAtNY Nm mu q hq) else ∅

theorem Anderson4D.maxFiberAtNY_eq {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : maxFiberAtNY Nm mu q = leavesAtNX Nm mu (maxNXAtNY Nm mu q hq)

def Anderson4D.isNormalizedCompound {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : Prop

The local normalization needed for the sentence "for such leaves m_l > 2" in the proof of (5.83).

Equations

• Anderson4D.isNormalizedCompound mu compound l = (↑l ∈ compound ∨ Anderson4D.leafMultiplicity mu l = 2)

@[implicit_reducible]

instance Anderson4D.instDecidableIsNormalizedCompound {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : Decidable (isNormalizedCompound mu compound l)

Equations

• Anderson4D.instDecidableIsNormalizedCompound mu compound l = id inferInstance

noncomputable def Anderson4D.normalizedSimpleMaxFiber {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Finset (HeppLeaf t)

Equations

• Anderson4D.normalizedSimpleMaxFiber Nm mu compound q = {l ∈ Anderson4D.maxFiberAtNY Nm mu q | ¬Anderson4D.isNormalizedCompound mu compound l}

noncomputable def Anderson4D.normalizedCompoundMaxFiber {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Finset (HeppLeaf t)

Equations

• Anderson4D.normalizedCompoundMaxFiber Nm mu compound q = {l ∈ Anderson4D.maxFiberAtNY Nm mu q | Anderson4D.isNormalizedCompound mu compound l}

theorem Anderson4D.normalizedFiber_union {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : normalizedSimpleMaxFiber Nm mu compound q ∪ normalizedCompoundMaxFiber Nm mu compound q = maxFiberAtNY Nm mu q

theorem Anderson4D.normalizedFiber_disjoint {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Disjoint (normalizedSimpleMaxFiber Nm mu compound q) (normalizedCompoundMaxFiber Nm mu compound q)

theorem Anderson4D.normalizedFiber_card {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : (normalizedSimpleMaxFiber Nm mu compound q).card + (normalizedCompoundMaxFiber Nm mu compound q).card = (maxFiberAtNY Nm mu q).card

theorem Anderson4D.normalizedSimple_multiplicity_gt_two {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) {l : HeppLeaf t} (hl : l ∈ normalizedSimpleMaxFiber Nm mu compound q) : 2 < leafMultiplicity mu l

The actual majority classifier (tie goes to simple)

def Anderson4D.isSimpleMajorityAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Prop

Equations

• Anderson4D.isSimpleMajorityAtNY Nm mu compound q = ((Anderson4D.normalizedCompoundMaxFiber Nm mu compound q).card ≤ (Anderson4D.normalizedSimpleMaxFiber Nm mu compound q).card)

@[implicit_reducible]

noncomputable instance Anderson4D.instDecidableIsSimpleMajorityAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Decidable (isSimpleMajorityAtNY Nm mu compound q)

Equations

• Anderson4D.instDecidableIsSimpleMajorityAtNY Nm mu compound q = id inferInstance

noncomputable def Anderson4D.majorityTagAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : Bool

false means simple majority and true means compound majority. Thus an exact tie is deterministically sent to false.

Equations

• Anderson4D.majorityTagAtNY Nm mu compound q = if Anderson4D.isSimpleMajorityAtNY Nm mu compound q then false else true

noncomputable def Anderson4D.simpleMajorityAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset NYClass

Equations

• Anderson4D.simpleMajorityAtP Nm mu compound P = Anderson4D.boolFiber (Anderson4D.nyAtP Nm mu P) (Anderson4D.majorityTagAtNY Nm mu compound) false

noncomputable def Anderson4D.compoundMajorityAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset NYClass

Equations

• Anderson4D.compoundMajorityAtP Nm mu compound P = Anderson4D.boolFiber (Anderson4D.nyAtP Nm mu P) (Anderson4D.majorityTagAtNY Nm mu compound) true

theorem Anderson4D.simpleMajorityAtP_union_compoundMajorityAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : simpleMajorityAtP Nm mu compound P ∪ compoundMajorityAtP Nm mu compound P = nyAtP Nm mu P

theorem Anderson4D.simpleMajorityAtP_disjoint_compoundMajorityAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Disjoint (simpleMajorityAtP Nm mu compound P) (compoundMajorityAtP Nm mu compound P)

theorem Anderson4D.mem_simpleMajorityAtP_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (q : NYClass) : q ∈ simpleMajorityAtP Nm mu compound P ↔ q ∈ nyAtP Nm mu P ∧ isSimpleMajorityAtNY Nm mu compound q

theorem Anderson4D.mem_compoundMajorityAtP_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (q : NYClass) : q ∈ compoundMajorityAtP Nm mu compound P ↔ q ∈ nyAtP Nm mu P ∧ (normalizedSimpleMaxFiber Nm mu compound q).card < (normalizedCompoundMaxFiber Nm mu compound q).card

The canonical increasing-N enumeration at fixed P

theorem Anderson4D.nyClass_N_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : 0 < q.1

theorem Anderson4D.nyAtP_fst_injOn {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Set.InjOn Prod.fst ↑(nyAtP Nm mu P)

At fixed P = YN⁴, the N coordinate determines (N,Y).

theorem Anderson4D.simpleMajorityAtP_fst_injOn {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Set.InjOn Prod.fst ↑(simpleMajorityAtP Nm mu compound P)

noncomputable def Anderson4D.fstImageEquiv (s : Finset (ℕ × ℕ)) (hinj : Set.InjOn Prod.fst ↑s) : ↥s ≃ ↥(Finset.image Prod.fst s)

A finite set on which Prod.fst is injective is equivalent to its image of first coordinates.

Equations

• Anderson4D.fstImageEquiv s hinj = Equiv.ofBijective (fun (q : ↥s) => ⟨(↑q).1, ⋯⟩) ⋯

@[simp]

theorem Anderson4D.fstImageEquiv_apply_val (s : Finset (ℕ × ℕ)) (hinj : Set.InjOn Prod.fst ↑s) (q : ↥s) : ↑((fstImageEquiv s hinj) q) = (↑q).1

noncomputable def Anderson4D.simpleMajorityIncreasingEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Fin (simpleMajorityAtP Nm mu compound P).card ≃ ↥(simpleMajorityAtP Nm mu compound P)

The actual increasing-N enumeration used in (5.83)--(5.84). It is obtained by sorting the image of the first coordinate and transporting back through fstImageEquiv.

Equations

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

theorem Anderson4D.simpleMajorityIncreasingEquiv_fst_strictMono {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : StrictMono fun (i : Fin (simpleMajorityAtP Nm mu compound P).card) => (↑((simpleMajorityIncreasingEquiv Nm mu compound P) i)).1

theorem Anderson4D.pow_two_succ_le_of_strictMono_dyadic {r : ℕ} (N : Fin r → ℕ) (hmono : StrictMono N) (hdyadic : ∀ (i : Fin r), IsDyadicNat (N i)) (htwo : ∀ (i : Fin r), 2 ≤ N i) (i : Fin r) : 2 ^ (↑i + 1) ≤ N i

A strictly increasing sequence of positive powers of two grows at least as 2^(i+1).

theorem Anderson4D.simpleMajorityIncreasingEquiv_scale_lower {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (i : Fin (simpleMajorityAtP Nm mu compound P).card) : 2 ^ (↑i + 1) ≤ (↑((simpleMajorityIncreasingEquiv Nm mu compound P) i)).1

Cardinal majority payoffs on the maximal fiber

theorem Anderson4D.maxFiberAtNY_card_lower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : q.2 ≤ (maxFiberAtNY Nm mu q).card

theorem Anderson4D.simpleMajority_card_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hS : isSimpleMajorityAtNY Nm mu compound q) : q.2 ≤ 2 * (normalizedSimpleMaxFiber Nm mu compound q).card

theorem Anderson4D.compoundMajority_card_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hC : ¬isSimpleMajorityAtNY Nm mu compound q) : q.2 ≤ 2 * (normalizedCompoundMaxFiber Nm mu compound q).card

Paper (5.82) with the actual classifier

theorem Anderson4D.fixedP_majority_partition_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Nat.multinomial (nyAtP Nm mu P) (multiplicityNY Nm mu) ≤ 2 ^ multiplicityP Nm mu P * Nat.multinomial (simpleMajorityAtP Nm mu compound P) (multiplicityNY Nm mu) * Nat.multinomial (compoundMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)

Paper (5.82), now specialized to the majority predicate defined from the canonical maxNXAtNY fiber. The exponent is exactly m_P.

The simple payoff: denominator-free (5.83)

def Anderson4D.simpleScaleExponent {t : PlaneTree} (mu : t.Multiplicities) (l : HeppLeaf t) : ℕ

Equations

• Anderson4D.simpleScaleExponent mu l = 2 * (Anderson4D.leafMultiplicity mu l - 2)

noncomputable def Anderson4D.simpleMajorityExponent {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : ℕ

Equations

• Anderson4D.simpleMajorityExponent Nm mu compound q = ∑ l ∈ Anderson4D.normalizedSimpleMaxFiber Nm mu compound q, Anderson4D.simpleScaleExponent mu l

theorem Anderson4D.mem_maxFiberAtNY_class {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ maxFiberAtNY Nm mu q) : singleScaleSigma1 Nm mu l = maxNXAtNY Nm mu q hq

theorem Anderson4D.mem_maxFiberAtNY_parent_scale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ maxFiberAtNY Nm mu q) : scaleN Nm (PlaneTree.parentV ↑l) = q.1

theorem Anderson4D.mem_maxFiberAtNY_dyadicFloor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ maxFiberAtNY Nm mu q) : dyadicFloor (leafMultiplicity mu l) = maxXAtNY Nm mu q

theorem Anderson4D.maxX_le_two_mul_simpleScaleExponent {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ normalizedSimpleMaxFiber Nm mu compound q) : maxXAtNY Nm mu q ≤ 2 * simpleScaleExponent mu l

theorem Anderson4D.simpleMajority_exponent_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hS : isSimpleMajorityAtNY Nm mu compound q) : maxXAtNY Nm mu q * q.2 ≤ 4 * simpleMajorityExponent Nm mu compound q

The exponent inequality in (5.83): X* Y ≤ 4 ∑_{simple in L_{N,X*}} 2(m_l-2).

noncomputable def Anderson4D.simpleMajorityScaleProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : ℝ

Equations

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

theorem Anderson4D.simpleMajorityScaleProduct_eq {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : simpleMajorityScaleProduct Nm mu compound q = ↑q.1 ^ simpleMajorityExponent Nm mu compound q

theorem Anderson4D.simpleMajority_scale_payoff_fourth {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hS : isSimpleMajorityAtNY Nm mu compound q) : ↑q.1 ^ (maxXAtNY Nm mu q * q.2) ≤ simpleMajorityScaleProduct Nm mu compound q ^ 4

Real-power form of (5.83). Raising the simple scale product to the fourth power pays N^(X*Y).

Paper (5.84), with an explicit increasing enumeration

theorem Anderson4D.simpleMajority_multinomial_le_ordered (α : ℝ) (hα : 1 < α) {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (e : Fin r ≃ ι) (m : ι → ℕ) : ↑(Nat.multinomial Finset.univ m) ≤ (α ^ ∑ i : Fin r, (↑i + 1) * m (e i)) * (α / (α - 1)) ^ ∑ i : ι, m i

The exact (5.84) inequality along an explicitly supplied enumeration e. The inequality itself holds for every enumeration; in the paper e is then chosen to enumerate the fixed-P classes by increasing N.

theorem Anderson4D.fixedP_simpleMajority_multinomial_le_ordered (α : ℝ) (hα : 1 < α) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) {r : ℕ} (e : Fin r ≃ ↥(simpleMajorityAtP Nm mu compound P)) : ↑(Nat.multinomial (simpleMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)) ≤ (α ^ ∑ i : Fin r, (↑i + 1) * multiplicityNY Nm mu ↑(e i)) * (α / (α - 1)) ^ ∑ q ∈ simpleMajorityAtP Nm mu compound P, multiplicityNY Nm mu q

Fixed-P specialization of (5.84). The carrier is the actual simple majority class from (5.82), and e is the paper's chosen ordering of it.

theorem Anderson4D.fixedP_simpleMajority_multinomial_le_increasing (α : ℝ) (hα : 1 < α) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ↑(Nat.multinomial (simpleMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)) ≤ (α ^ ∑ i : Fin (simpleMajorityAtP Nm mu compound P).card, (↑i + 1) * multiplicityNY Nm mu ↑((simpleMajorityIncreasingEquiv Nm mu compound P) i)) * (α / (α - 1)) ^ ∑ q ∈ simpleMajorityAtP Nm mu compound P, multiplicityNY Nm mu q

(5.84) instantiated with the canonical increasing-N enumeration.

Closing the simple-majority factor with an explicit uniform α

noncomputable def Anderson4D.outerMajorityAlpha : ℝ

An explicit choice close enough to one for the absorption after (5.84). The denominator is deliberately a power of two.

Equations

• Anderson4D.outerMajorityAlpha = 65 / 64

theorem Anderson4D.one_lt_outerMajorityAlpha : 1 < outerMajorityAlpha

theorem Anderson4D.outerMajorityAlpha_div_sub_one : outerMajorityAlpha / (outerMajorityAlpha - 1) = 65

theorem Anderson4D.outerMajorityAlpha_pow_32_le_two : outerMajorityAlpha ^ 32 ≤ 2

theorem Anderson4D.simpleMajority_weighted_alpha_point_le {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (i : Fin (simpleMajorityAtP Nm mu compound P).card) : outerMajorityAlpha ^ ((↑i + 1) * multiplicityNY Nm mu ↑((simpleMajorityIncreasingEquiv Nm mu compound P) i)) ≤ simpleMajorityScaleProduct Nm mu compound ↑((simpleMajorityIncreasingEquiv Nm mu compound P) i)

Pointwise absorption of the weighted α factor in (5.84) by the simple scale payoff from (5.83).

theorem Anderson4D.fixedP_simpleMajority_multinomial_le_scaleProduct {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ↑(Nat.multinomial (simpleMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)) ≤ (65 ^ ∑ q ∈ simpleMajorityAtP Nm mu compound P, multiplicityNY Nm mu q) * ∏ q ∈ simpleMajorityAtP Nm mu compound P, simpleMajorityScaleProduct Nm mu compound q

The completed simple-majority estimate from (5.83)--(5.84). The remaining factor is exactly the product of the local normalized simple scale payoffs; all combinatorial loss is 65 to the total simple mass.

The compound carrier grouped by X*

noncomputable def Anderson4D.compoundXCarrierAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset ℕ

Equations

• Anderson4D.compoundXCarrierAtP Nm mu compound P = Finset.image (fun (q : Anderson4D.NYClass) => Anderson4D.maxXAtNY Nm mu q) (Anderson4D.compoundMajorityAtP Nm mu compound P)

noncomputable def Anderson4D.compoundAtPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : Finset NYClass

Equations

• Anderson4D.compoundAtPX Nm mu compound P X = {q ∈ Anderson4D.compoundMajorityAtP Nm mu compound P | Anderson4D.maxXAtNY Nm mu q = X}

noncomputable def Anderson4D.compoundMultiplicityPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : ℕ

Equations

• Anderson4D.compoundMultiplicityPX Nm mu compound P X = ∑ q ∈ Anderson4D.compoundAtPX Nm mu compound P X, Anderson4D.multiplicityNY Nm mu q

noncomputable def Anderson4D.compoundYMassPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : ℕ

Equations

• Anderson4D.compoundYMassPX Nm mu compound P X = ∑ q ∈ Anderson4D.compoundAtPX Nm mu compound P X, q.2

theorem Anderson4D.compoundAtPX_subset_nyAtPX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : compoundAtPX Nm mu compound P X ⊆ nyAtPX Nm mu P X

theorem Anderson4D.compoundAtPX_active {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {P X : ℕ} {q : NYClass} (hq : q ∈ compoundAtPX Nm mu compound P X) : q ∈ nyCarrier Nm mu

theorem Anderson4D.compoundAtPX_maxX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {P X : ℕ} {q : NYClass} (hq : q ∈ compoundAtPX Nm mu compound P X) : maxXAtNY Nm mu q = X

theorem Anderson4D.compoundMajorityAtP_mapsTo_X {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) {q : NYClass} (hq : q ∈ compoundMajorityAtP Nm mu compound P) : maxXAtNY Nm mu q ∈ compoundXCarrierAtP Nm mu compound P

theorem Anderson4D.compoundMass_eq_sum_PX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ∑ q ∈ compoundMajorityAtP Nm mu compound P, multiplicityNY Nm mu q = ∑ X ∈ compoundXCarrierAtP Nm mu compound P, compoundMultiplicityPX Nm mu compound P X

theorem Anderson4D.compoundMultiplicityPX_bounds {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : X * compoundYMassPX Nm mu compound P X ≤ compoundMultiplicityPX Nm mu compound P X ∧ compoundMultiplicityPX Nm mu compound P X ≤ 8 * X * compoundYMassPX Nm mu compound P X

theorem Anderson4D.compoundXCarrier_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {P X : ℕ} (hX : X ∈ compoundXCarrierAtP Nm mu compound P) : IsDyadicNat X

theorem Anderson4D.compoundXCarrier_pos {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {P X : ℕ} (hX : X ∈ compoundXCarrierAtP Nm mu compound P) : 0 < X

theorem Anderson4D.two_le_nxClass_X_of_active {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : 2 ≤ a.2

theorem Anderson4D.compoundXCarrier_two_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {P X : ℕ} (hX : X ∈ compoundXCarrierAtP Nm mu compound P) : 2 ≤ X

noncomputable def Anderson4D.compoundXIncreasingEquiv {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Fin (compoundXCarrierAtP Nm mu compound P).card ≃ ↥(compoundXCarrierAtP Nm mu compound P)

Increasing enumeration of the distinct compound X* values.

Equations

• Anderson4D.compoundXIncreasingEquiv Nm mu compound P = ↑((Anderson4D.compoundXCarrierAtP Nm mu compound P).orderIsoOfFin ⋯)

theorem Anderson4D.compoundXIncreasingEquiv_scale_lower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (i : Fin (compoundXCarrierAtP Nm mu compound P).card) : 2 ^ (↑i + 1) ≤ ↑((compoundXIncreasingEquiv Nm mu compound P) i)

theorem Anderson4D.compound_fixedP_multinomial_decomposition {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Nat.multinomial (compoundMajorityAtP Nm mu compound P) (multiplicityNY Nm mu) = Nat.multinomial (compoundXCarrierAtP Nm mu compound P) (compoundMultiplicityPX Nm mu compound P) * ∏ X ∈ compoundXCarrierAtP Nm mu compound P, Nat.multinomial (compoundAtPX Nm mu compound P X) (multiplicityNY Nm mu)

theorem Anderson4D.compoundMultiplicityNY_lacunary_fixed_X {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : Lacunary 4 (compoundAtPX Nm mu compound P X) (multiplicityNY Nm mu)

theorem Anderson4D.compoundWithinPX_multinomial_product_le : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ), ↑(∏ X ∈ compoundXCarrierAtP Nm mu compound P, Nat.multinomial (compoundAtPX Nm mu compound P X) (multiplicityNY Nm mu)) ≤ C ^ ∑ q ∈ compoundMajorityAtP Nm mu compound P, multiplicityNY Nm mu q

noncomputable def Anderson4D.compoundOuterAlpha : ℝ

Equations

• Anderson4D.compoundOuterAlpha = 129 / 128

theorem Anderson4D.one_lt_compoundOuterAlpha : 1 < compoundOuterAlpha

theorem Anderson4D.compoundOuterAlpha_div_sub_one : compoundOuterAlpha / (compoundOuterAlpha - 1) = 129

theorem Anderson4D.compoundOuterAlpha_pow_64_le_two : compoundOuterAlpha ^ 64 ≤ 2

noncomputable def Anderson4D.compoundBlockPayoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : ℝ

Equations

• Anderson4D.compoundBlockPayoff Nm mu compound P X = ↑X ^ (↑(X * Anderson4D.compoundYMassPX Nm mu compound P X) / 8)

theorem Anderson4D.compoundBlockPayoff_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P X : ℕ) : 0 ≤ compoundBlockPayoff Nm mu compound P X

theorem Anderson4D.compoundOuter_weighted_alpha_point_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) (i : Fin (compoundXCarrierAtP Nm mu compound P).card) : compoundOuterAlpha ^ ((↑i + 1) * compoundMultiplicityPX Nm mu compound P ↑((compoundXIncreasingEquiv Nm mu compound P) i)) ≤ compoundBlockPayoff Nm mu compound P ↑((compoundXIncreasingEquiv Nm mu compound P) i)

Pointwise absorption used in the last application of (5.50) in (5.86).

theorem Anderson4D.compoundBlock_multinomial_le_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ↑(Nat.multinomial (compoundXCarrierAtP Nm mu compound P) (compoundMultiplicityPX Nm mu compound P)) ≤ (129 ^ ∑ X ∈ compoundXCarrierAtP Nm mu compound P, compoundMultiplicityPX Nm mu compound P X) * ∏ X ∈ compoundXCarrierAtP Nm mu compound P, compoundBlockPayoff Nm mu compound P X

The block-mass multinomial in (5.86), with an explicit constant 129.

After the lacunary within-block factors, (5.86) is now reduced to the explicit block payoff. The next theorem packages both parts.

theorem Anderson4D.compoundMajority_multinomial_le_blockPayoff : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ), ↑(Nat.multinomial (compoundMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)) ≤ (C ^ ∑ q ∈ compoundMajorityAtP Nm mu compound P, multiplicityNY Nm mu q) * ∏ X ∈ compoundXCarrierAtP Nm mu compound P, compoundBlockPayoff Nm mu compound P X

The compound payoff: (5.85) and (5.86)

noncomputable def Anderson4D.compoundMajorityMass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : ℕ

Equations

• Anderson4D.compoundMajorityMass Nm mu compound q = ∑ l ∈ Anderson4D.normalizedCompoundMaxFiber Nm mu compound q, Anderson4D.leafMultiplicity mu l

noncomputable def Anderson4D.compoundMajorityFactorialProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : ℕ

Equations

• Anderson4D.compoundMajorityFactorialProduct Nm mu compound q = ∏ l ∈ Anderson4D.normalizedCompoundMaxFiber Nm mu compound q, (Anderson4D.leafMultiplicity mu l).factorial

theorem Anderson4D.maxX_le_leafMultiplicity_of_mem_maxFiber {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ maxFiberAtNY Nm mu q) : maxXAtNY Nm mu q ≤ leafMultiplicity mu l

theorem Anderson4D.compoundMajorityMass_le_multiplicityNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : compoundMajorityMass Nm mu compound q ≤ multiplicityNY Nm mu q

theorem Anderson4D.compound_point_factorial_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ normalizedCompoundMaxFiber Nm mu compound q) : maxXAtNY Nm mu q ^ maxXAtNY Nm mu q ≤ 4 ^ leafMultiplicity mu l * (leafMultiplicity mu l).factorial

theorem Anderson4D.compound_product_factorial_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : maxXAtNY Nm mu q ^ (maxXAtNY Nm mu q * (normalizedCompoundMaxFiber Nm mu compound q).card) ≤ 4 ^ compoundMajorityMass Nm mu compound q * compoundMajorityFactorialProduct Nm mu compound q

theorem Anderson4D.compoundMajority_factorial_certificate {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hC : ¬isSimpleMajorityAtNY Nm mu compound q) : maxXAtNY Nm mu q ^ (maxXAtNY Nm mu q * q.2) ≤ 16 ^ multiplicityNY Nm mu q * compoundMajorityFactorialProduct Nm mu compound q ^ 2

An eighth-power, denominator-free form of paper (5.85):

X^(X Y) ≤ 16^m_{N,Y} (∏_{compound in L_{N,X*}} m_l!)².

Taking eighth roots gives the printed quarter-factorial payoff, with an exponential loss. Keeping the statement integral avoids hiding positivity or rounding obligations in Real.rpow.

noncomputable def Anderson4D.compoundMajorityQuarterProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : ℝ

Equations

• Anderson4D.compoundMajorityQuarterProduct Nm mu compound q = ∏ l ∈ Anderson4D.normalizedCompoundMaxFiber Nm mu compound q, ↑(Anderson4D.leafMultiplicity mu l).factorial ^ (1 / 4)

noncomputable def Anderson4D.compoundMajorityRootLoss (m : ℕ) : ℝ

Explicit exponential loss used when taking the eighth root of the integral (5.85) certificate.

Equations

• Anderson4D.compoundMajorityRootLoss m = (16 ^ m) ^ (1 / 8)

theorem Anderson4D.quarterFactorial_pow_eight (k : ℕ) : (↑k.factorial ^ (1 / 4)) ^ 8 = ↑k.factorial ^ 2

theorem Anderson4D.compoundMajorityQuarterProduct_pow_eight {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : compoundMajorityQuarterProduct Nm mu compound q ^ 8 = ↑(compoundMajorityFactorialProduct Nm mu compound q) ^ 2

theorem Anderson4D.compoundMajorityRootLoss_pow_eight (m : ℕ) : compoundMajorityRootLoss m ^ 8 = 16 ^ m

theorem Anderson4D.compoundMajorityRootLoss_nonneg (m : ℕ) : 0 ≤ compoundMajorityRootLoss m

theorem Anderson4D.compoundMajorityQuarterProduct_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (q : NYClass) : 0 ≤ compoundMajorityQuarterProduct Nm mu compound q

theorem Anderson4D.compoundMajority_quarter_payoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) (hC : ¬isSimpleMajorityAtNY Nm mu compound q) : ↑(maxXAtNY Nm mu q) ^ (↑(maxXAtNY Nm mu q * q.2) / 8) ≤ compoundMajorityRootLoss (multiplicityNY Nm mu q) * compoundMajorityQuarterProduct Nm mu compound q

The printed quarter-power form of (5.85), with an explicit exponential loss. This discharges the real-root/positivity boundary of the integral certificate above.

theorem Anderson4D.compoundMajorityRootLoss_le_two_pow (m : ℕ) : compoundMajorityRootLoss m ≤ 2 ^ m

noncomputable def Anderson4D.compoundClassScalePayoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : ℝ

Equations

• Anderson4D.compoundClassScalePayoff Nm mu q = ↑(Anderson4D.maxXAtNY Nm mu q) ^ (↑(Anderson4D.maxXAtNY Nm mu q * q.2) / 8)

theorem Anderson4D.compoundBlockPayoff_eq_class_product {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) {X : ℕ} (hX : X ∈ compoundXCarrierAtP Nm mu compound P) : compoundBlockPayoff Nm mu compound P X = ∏ q ∈ compoundAtPX Nm mu compound P X, compoundClassScalePayoff Nm mu q

theorem Anderson4D.compoundBlockPayoff_product_eq_classProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ∏ X ∈ compoundXCarrierAtP Nm mu compound P, compoundBlockPayoff Nm mu compound P X = ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundClassScalePayoff Nm mu q

theorem Anderson4D.compoundClassScalePayoff_le_quarter {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) {q : NYClass} (hq : q ∈ compoundMajorityAtP Nm mu compound P) : compoundClassScalePayoff Nm mu q ≤ compoundMajorityRootLoss (multiplicityNY Nm mu q) * compoundMajorityQuarterProduct Nm mu compound q

theorem Anderson4D.compoundClassPayoff_product_le_quarter {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundClassScalePayoff Nm mu q ≤ (2 ^ ∑ q ∈ compoundMajorityAtP Nm mu compound P, multiplicityNY Nm mu q) * ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q

theorem Anderson4D.fixedP_compoundMajority_multinomial_le_quarterProduct : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ), ↑(Nat.multinomial (compoundMajorityAtP Nm mu compound P) (multiplicityNY Nm mu)) ≤ (C ^ ∑ q ∈ compoundMajorityAtP Nm mu compound P, multiplicityNY Nm mu q) * ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q

Completed compound-majority estimate (5.85)--(5.86), before the final disjoint-leaf product embedding into the frozen Proposition 5.10 payoff.

theorem Anderson4D.fixedP_majority_multinomial_le_localPayoff : ∃ (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 (nyAtP Nm mu P) (multiplicityNY Nm mu)) ≤ (C ^ multiplicityP Nm mu P * ∏ q ∈ simpleMajorityAtP Nm mu compound P, simpleMajorityScaleProduct Nm mu compound q) * ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q

The fixed-P assembly of (5.82)--(5.86). The two majority pieces are recombined with a single constant to the full mass m_P; the remaining factors are exactly the normalized simple and compound leaf-local payoffs.

Honest treatment of the m_l = 2 normalization

noncomputable def Anderson4D.quarterFactorial (k : ℕ) : ℝ

Equations

• Anderson4D.quarterFactorial k = ↑k.factorial ^ (1 / 4)

noncomputable def Anderson4D.originalOuterLeafPayoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : ℝ

Equations

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

noncomputable def Anderson4D.normalizedOuterLeafPayoff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : ℝ

Equations

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

theorem Anderson4D.quarterFactorial_two_le_two : quarterFactorial 2 ≤ 2

theorem Anderson4D.normalizedOuterLeafPayoff_le_two_mul_original {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : normalizedOuterLeafPayoff Nm mu compound l ≤ 2 * originalOuterLeafPayoff Nm mu compound l

theorem Anderson4D.normalizedOuterLeafPayoff_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : 0 ≤ normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.quarterFactorial_one_le (k : ℕ) : 1 ≤ quarterFactorial k

theorem Anderson4D.normalizedOuterLeafPayoff_one_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : 1 ≤ normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.mem_maxFiberAtNY_nyClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ maxFiberAtNY Nm mu q) : singleScaleSigma2 Nm mu (singleScaleSigma1 Nm mu l) = q

theorem Anderson4D.maxFiberAtNY_disjoint_of_ne {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q r : NYClass} (hq : q ∈ nyCarrier Nm mu) (hr : r ∈ nyCarrier Nm mu) (hqr : q ≠ r) : Disjoint (maxFiberAtNY Nm mu q) (maxFiberAtNY Nm mu r)

noncomputable def Anderson4D.simpleMajorityLeafCarrierAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset (HeppLeaf t)

Equations

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

noncomputable def Anderson4D.compoundMajorityLeafCarrierAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset (HeppLeaf t)

Equations

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

noncomputable def Anderson4D.majorityLeafCarrierAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Finset (HeppLeaf t)

Equations

• Anderson4D.majorityLeafCarrierAtP Nm mu compound P = Anderson4D.simpleMajorityLeafCarrierAtP Nm mu compound P ∪ Anderson4D.compoundMajorityLeafCarrierAtP Nm mu compound P

theorem Anderson4D.simpleMajorityMaxFibers_pairwiseDisjoint {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : (↑(simpleMajorityAtP Nm mu compound P)).PairwiseDisjoint (normalizedSimpleMaxFiber Nm mu compound)

theorem Anderson4D.compoundMajorityMaxFibers_pairwiseDisjoint {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : (↑(compoundMajorityAtP Nm mu compound P)).PairwiseDisjoint (normalizedCompoundMaxFiber Nm mu compound)

theorem Anderson4D.simpleMajorityLeafCarrier_disjoint_compound {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : Disjoint (simpleMajorityLeafCarrierAtP Nm mu compound P) (compoundMajorityLeafCarrierAtP Nm mu compound P)

theorem Anderson4D.simpleMajorityScaleProduct_product_eq_leafCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ∏ q ∈ simpleMajorityAtP Nm mu compound P, simpleMajorityScaleProduct Nm mu compound q = ∏ l ∈ simpleMajorityLeafCarrierAtP Nm mu compound P, normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.compoundMajorityQuarterProduct_product_eq_leafCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q = ∏ l ∈ compoundMajorityLeafCarrierAtP Nm mu compound P, normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.localMajorityPayoff_eq_leafCarrierProduct {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : (∏ q ∈ simpleMajorityAtP Nm mu compound P, simpleMajorityScaleProduct Nm mu compound q) * ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q = ∏ l ∈ majorityLeafCarrierAtP Nm mu compound P, normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.simpleMajorityLeafCarrier_subset_leavesAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : simpleMajorityLeafCarrierAtP Nm mu compound P ⊆ leavesAtP Nm mu P

theorem Anderson4D.compoundMajorityLeafCarrier_subset_leavesAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : compoundMajorityLeafCarrierAtP Nm mu compound P ⊆ leavesAtP Nm mu P

theorem Anderson4D.majorityLeafCarrier_subset_leavesAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : majorityLeafCarrierAtP Nm mu compound P ⊆ leavesAtP Nm mu P

theorem Anderson4D.localMajorityPayoff_le_normalizedLeavesAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (P : ℕ) : (∏ q ∈ simpleMajorityAtP Nm mu compound P, simpleMajorityScaleProduct Nm mu compound q) * ∏ q ∈ compoundMajorityAtP Nm mu compound P, compoundMajorityQuarterProduct Nm mu compound q ≤ ∏ l ∈ leavesAtP Nm mu P, normalizedOuterLeafPayoff Nm mu compound l

theorem Anderson4D.originalOuterLeafPayoff_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (l : HeppLeaf t) : 0 ≤ originalOuterLeafPayoff Nm mu compound l

theorem Anderson4D.normalizedMajorityPayoff_finset_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (s : Finset (HeppLeaf t)) : ∏ l ∈ s, normalizedOuterLeafPayoff Nm mu compound l ≤ 2 ^ s.card * ∏ l ∈ s, originalOuterLeafPayoff Nm mu compound l

The multiplicity-two normalization bound on an arbitrary leaf carrier. Keeping the carrier explicit is essential before multiplying the fixed-P estimates over distinct values of P.

theorem Anderson4D.leavesAtP_card_le_multiplicityP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : (leavesAtP Nm mu P).card ≤ multiplicityP Nm mu P

theorem Anderson4D.fixedP_majority_multinomial_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 (nyAtP Nm mu P) (multiplicityNY Nm mu)) ≤ C ^ multiplicityP Nm mu P * ∏ l ∈ leavesAtP Nm mu P, originalOuterLeafPayoff Nm mu compound l

The completed fixed-P outer-majority estimate (5.82)--(5.86), including the canonical-fiber disjointness ledger and the honest m_l = 2 normalization. No selected fiber is duplicated, and the final payoff is restricted to the paper's exact carrier L_P.

theorem Anderson4D.normalizedMajorityPayoff_le {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : ∏ l : HeppLeaf t, normalizedOuterLeafPayoff Nm mu compound l ≤ 2 ^ Fintype.card (HeppLeaf t) * ∏ l : HeppLeaf t, originalOuterLeafPayoff Nm mu compound l

Relabeling the multiplicity-two simple leaves costs at most 2^|L|. This is the explicit constant absorption omitted in the prose of the paper.

Downstream integration boundary

Equations (5.83)--(5.86), their recombination with (5.82), canonical-fiber disjointness, and the m_l = 2 normalization are all closed above by fixedP_majority_multinomial_le_originalPayoff.

The next assembly file must first compose this (N,Y)-multinomial bound with fixedP_multinomial_le_outerNY, whose left side is the required (N,X) multinomial. It must then multiply the resulting fixed-P bound over the finite outer P carrier and identify the disjoint leavesAtP products with the single global leaf product in Proposition 5.10. These two interface steps are downstream of, rather than missing steps in, (5.83)--(5.86).