Assembly bridge for the single-scale estimate

This file connects the finite (N,X,Y,P) classification in SingleScaleSetup to the analytic skipped-edge estimates in SingleScaleMixed. Each analytic cluster remains the image of one (N,X) fiber. In particular, an (N,Y) class is represented by its canonical maximal-X fiber, never by the union of all its fibers.

Root-budget certificates

theorem Anderson4D.XYCluster.nxClassCluster_RNDominance_one {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : RNDominance 1 (↑R) (nxClassCluster ht hroot Nm mu z hz a ha)

The raw root-budget estimate for an active (N,X) fiber, packaged in the exact interface consumed by the constant-one mixed estimate.

theorem Anderson4D.XYCluster.nyClassCluster_RNDominance_two {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : RNDominance 2 (↑R) (nyClassCluster ht hroot Nm mu z hz q hq)

Safe constant-two weakening for the coarse (N,Y) representative. The exact-cardinality root budget already gives constant-one dominance for its chosen maximal-X fiber; 2 is exposed only as an assembly-safe weakening, not as a necessary dyadic-cardinality loss.

theorem Anderson4D.XYCluster.nxClassCluster_points_nonempty {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : (nxClassCluster ht hroot Nm mu z hz a ha).points.Nonempty

Every active (N,X) cluster has a point.

theorem Anderson4D.XYCluster.nxClassCluster_one_le_X {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : 1 ≤ (nxClassCluster ht hroot Nm mu z hz a ha).X

The dyadic multiplicity weight of every active (N,X) cluster is at least one.

From labeled copies to the point carrier

The paper's permutation word contains mu.m l distinct copies of a leaf l, whereas Lemma 5.14 sums once over its lattice point. On an active (N,X) fiber these quantities are comparable but not equal: X ≤ mu.m l < 2X. The definitions and bounds below preserve the actual multiplicity and expose one factor 2 for every independently chosen copy.

def Anderson4D.XYCluster.nxCopyWeightedSum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (a : NXClass) (f : (Fin 4 → ℤ) → ℝ) : ℝ

A weighted sum over the distinct copies in one (N,X) fiber, written without inventing labels: the weight at z l is repeated mu.m l times.

Equations

• Anderson4D.XYCluster.nxCopyWeightedSum Nm mu z a f = ∑ l ∈ Anderson4D.leavesAtNX Nm mu a, ↑(Anderson4D.leafMultiplicity mu l) * f (z l)

def Anderson4D.XYCluster.nxPointWeightedSum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (a : NXClass) (f : (Fin 4 → ℤ) → ℝ) : ℝ

The corresponding point-level sum, with each embedded leaf counted once.

Equations

• Anderson4D.XYCluster.nxPointWeightedSum Nm mu z a f = ∑ x ∈ Anderson4D.nxClassPoints Nm mu z a, f x

theorem Anderson4D.XYCluster.leafMultiplicity_lt_two_mul_nxClass_X {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (_ha : a ∈ nxCarrier Nm mu) {l : HeppLeaf t} (hl : l ∈ leavesAtNX Nm mu a) : leafMultiplicity mu l < 2 * a.2

Exact paper fact behind the copies-to-points conversion: an actual leaf multiplicity is strictly smaller than twice its dyadic bucket value.

theorem Anderson4D.XYCluster.nxCopyWeightedSum_le_two_mul_pointWeightedSum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (f : (Fin 4 → ℤ) → ℝ) (hf : ∀ x ∈ nxClassPoints Nm mu z a, 0 ≤ f x) : nxCopyWeightedSum Nm mu z a f ≤ 2 * (↑a.2 * nxPointWeightedSum Nm mu z a f)

One copy variable costs at most 2 after the analytic X factor is pulled out. The weight is allowed to depend on the embedded lattice point.

def Anderson4D.XYCluster.nxCopyChoiceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : ℕ

Number of actual labeled-copy choices in one active fiber.

Equations

• Anderson4D.XYCluster.nxCopyChoiceCount Nm mu a = ∑ l ∈ Anderson4D.leavesAtNX Nm mu a, Anderson4D.leafMultiplicity mu l

def Anderson4D.XYCluster.nxPointChoiceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (a : NXClass) : ℕ

Number of point choices after pulling out the dyadic multiplicity X.

Equations

• Anderson4D.XYCluster.nxPointChoiceCount Nm mu z a = a.2 * (Anderson4D.nxClassPoints Nm mu z a).card

theorem Anderson4D.XYCluster.nxCopyChoiceCount_le_two_mul_pointChoiceCount {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : Function.Injective z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : nxCopyChoiceCount Nm mu a ≤ 2 * nxPointChoiceCount Nm mu z a

Counting specialization of the one-variable copies-to-points bound. It uses the actual mu.m l; no multiplicity is identified with X.

theorem Anderson4D.XYCluster.nxCopyChoiceCount_pow_le_two_pow_mul_pointChoiceCount_pow {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : Function.Injective z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (k : ℕ) : nxCopyChoiceCount Nm mu a ^ k ≤ 2 ^ k * nxPointChoiceCount Nm mu z a ^ k

k independent copy choices incur the explicit loss 2^k.

theorem Anderson4D.XYCluster.nxCopyWeightedChoice_le_two_pow_mul_pointWeightedChoice {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (k : ℕ) (f : Fin k → (Fin 4 → ℤ) → ℝ) (hf : ∀ (i : Fin k), ∀ x ∈ nxClassPoints Nm mu z a, 0 ≤ f i x) : ∏ i : Fin k, nxCopyWeightedSum Nm mu z a (f i) ≤ 2 ^ k * ∏ i : Fin k, ↑a.2 * nxPointWeightedSum Nm mu z a (f i)

Weighted k-variable version. This is the reusable interface for replacing independent labeled-copy sums by Lemma 5.14 point sums.

The coupled two-copy sum used in (5.91)

noncomputable def Anderson4D.XYCluster.nxCoupledCopyPairSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) (u : Fin 4 → ℤ) : ℝ

The unrestricted nested sum over the actual labeled copies in two possibly different (N,X) fibers. This is the copy-level left-hand side that dominates the corresponding conditional permutation sum: forgetting which labeled copies have already been used only enlarges a nonnegative sum.

Equations

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

theorem Anderson4D.XYCluster.nxCoupledCopyPairSum_le_four_mul_mixedPairInner {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) (u : Fin 4 → ℤ) : nxCoupledCopyPairSum ht hroot Nm mu z hz R ha hb skipA skipB u ≤ 4 * (nxClassCluster ht hroot Nm mu z hz a ha).mixedPairInner (nxClassCluster ht hroot Nm mu z hz b hb) R skipA skipB u

Replacing the two actual copy variables by their point carriers costs at most 2² = 4. The proof is nested, so the second edge may genuinely depend on the first point; no false product-separability assumption is used.

Uniform local assembly

theorem Anderson4D.XYCluster.nxClassClusters_mixedPairInner_le_5_91 : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) (u : Fin 4 → ℤ), (nxClassCluster ht hroot Nm mu z hz a ha).mixedPairInner (nxClassCluster ht hroot Nm mu z hz b hb) (↑R) skipA skipB u ≤ C * (nxClassCluster ht hroot Nm mu z hz a ha).mixedTarget (nxClassCluster ht hroot Nm mu z hz b hb) skipA skipB

Uniform form of (5.91) for arbitrary active (N,X) fibers. The existential constant is outside every tree, class, embedding, and skip choice, so later finite sums may use it without choosing a new constant for each fiber.

theorem Anderson4D.XYCluster.nyClassClusters_mixedPairInner_le_5_91 : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ {q r : NYClass} (hq : q ∈ nyCarrier Nm mu) (hr : r ∈ nyCarrier Nm mu) (skipQ skipR : Bool) (u : Fin 4 → ℤ), (nyClassCluster ht hroot Nm mu z hz q hq).mixedPairInner (nyClassCluster ht hroot Nm mu z hz r hr) (↑R) skipQ skipR u ≤ C * (nyClassCluster ht hroot Nm mu z hz q hq).mixedTarget (nyClassCluster ht hroot Nm mu z hz r hr) skipQ skipR

Representative-only convenience bound for active (N,Y) classes. It estimates the canonical maximal-X fiber used in the coarse (5.75) ledger. It must not replace the arbitrary (N,X) fibers occurring in the fixed-X inner sum (5.87).

Actual-volume versus dyadic-volume gain

def Anderson4D.XYCluster.dyadicP (q : NYClass) : ℝ

The paper's dyadic volume P = Y N⁴, cast to the analytic value type.

Equations

• Anderson4D.XYCluster.dyadicP q = ↑(Anderson4D.singleScaleSigma3 q)

noncomputable def Anderson4D.XYCluster.dyadicForwardGain (q r : NYClass) : ℝ

The dyadic gain in (5.87)/(5.91), with exponent 1/8. The separate outer estimate (5.76) uses θ = 1/20.

Equations

• Anderson4D.XYCluster.dyadicForwardGain q r = min 1 ((Anderson4D.XYCluster.dyadicP r / Anderson4D.XYCluster.dyadicP q) ^ (1 / 8))

theorem Anderson4D.XYCluster.dyadicP_pos {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : 0 < dyadicP q

An active dyadic class has strictly positive paper volume.

theorem Anderson4D.XYCluster.dyadicForwardGain_nonneg (q r : NYClass) : 0 ≤ dyadicForwardGain q r

The exact dyadic target printed in (5.91)

def Anderson4D.XYCluster.paperDyadicY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : ℝ

The dyadic point-count parameter Y belonging to an (N,X) fiber.

Equations

• Anderson4D.XYCluster.paperDyadicY Nm mu a = ↑(Anderson4D.singleScaleSigma2 Nm mu a).2

noncomputable def Anderson4D.XYCluster.paperDyadicBase {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : ℝ

The unskipped local factor X Y^(1/2) N⁻² in (5.91), using the paper's original scale N, not the analytic separation scale N/2.

Equations

• Anderson4D.XYCluster.paperDyadicBase Nm mu a = ↑a.2 * √(Anderson4D.XYCluster.paperDyadicY Nm mu a) * (↑a.1)⁻¹ ^ 2

noncomputable def Anderson4D.XYCluster.paperDyadicSkipXi {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : ℝ

The paper's factor Ξ = (XY)⁻¹/² when the incoming edge is skipped.

Equations

• Anderson4D.XYCluster.paperDyadicSkipXi Nm mu a skipped = if skipped = true then (√(↑a.2 * Anderson4D.XYCluster.paperDyadicY Nm mu a))⁻¹ else 1

noncomputable def Anderson4D.XYCluster.paperDyadicLocalTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : ℝ

One exact local factor on the right-hand side of (5.91).

Equations

• Anderson4D.XYCluster.paperDyadicLocalTarget Nm mu a skipped = Anderson4D.XYCluster.paperDyadicBase Nm mu a * Anderson4D.XYCluster.paperDyadicSkipXi Nm mu a skipped

noncomputable def Anderson4D.XYCluster.paperDyadicPairTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a b : NXClass) (skipA skipB : Bool) : ℝ

The exact two-cluster dyadic target on the right-hand side of (5.91).

Equations

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

theorem Anderson4D.XYCluster.paperDyadicLocalTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (skipped : Bool) : 0 ≤ paperDyadicLocalTarget Nm mu a skipped

theorem Anderson4D.XYCluster.paperDyadicPairTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a b : NXClass) (skipA skipB : Bool) : 0 ≤ paperDyadicPairTarget Nm mu a b skipA skipB

theorem Anderson4D.XYCluster.nxClassCluster_forwardGain_le_dyadicForwardGain {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) : (nxClassCluster ht hroot Nm mu z hz a ha).forwardGain (nxClassCluster ht hroot Nm mu z hz b hb) ≤ 2 ^ (1 / 8) * dyadicForwardGain (singleScaleSigma2 Nm mu a) (singleScaleSigma2 Nm mu b)

The actual Lemma 5.14 gain for arbitrary active (N,X) fibers is controlled by the dyadic P = YN⁴ gain attached to their own σ₂ classes. No maximal-X representative is substituted.

theorem Anderson4D.XYCluster.nxClassCluster_mixedTarget_le_paperDyadicPairTarget {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) : (nxClassCluster ht hroot Nm mu z hz a ha).mixedTarget (nxClassCluster ht hroot Nm mu z hz b hb) skipA skipB ≤ 128 * paperDyadicPairTarget Nm mu a b skipA skipB

The analytic target built from actual point-cardinalities and the separation scale N/2 is bounded by a universal multiple of the exact dyadic target printed in (5.91). The constant audit is:

• at most 8 per local factor (4 from (N/2)⁻², at most 2 from replacing sqrt |L_{N,X}| by sqrt Y; skipped Ξ only improves);
• at most 2 for the 1/8-power volume gain.

Thus 8 · 8 · 2 = 128.

theorem Anderson4D.XYCluster.nxCoupledCopyPairSum_le_paperDyadicPairTarget : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (skipA skipB : Bool) (u : Fin 4 → ℤ), nxCoupledCopyPairSum ht hroot Nm mu z hz (↑R) ha hb skipA skipB u ≤ C * paperDyadicPairTarget Nm mu a b skipA skipB

Uniform copy-level form of the local estimate (5.91), with the existential constant outside every tree, class, embedding, scale, skip choice, and fixed preceding point. Its left-hand side uses the actual leaf multiplicities; its right-hand side is the paper's exact dyadic X,Y,N,Ξ,P target.

theorem Anderson4D.XYCluster.nyClassCluster_forwardGain_le_dyadicForwardGain {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {q r : NYClass} (hq : q ∈ nyCarrier Nm mu) (hr : r ∈ nyCarrier Nm mu) : (nyClassCluster ht hroot Nm mu z hz q hq).forwardGain (nyClassCluster ht hroot Nm mu z hz r hr) ≤ 2 ^ (1 / 8) * dyadicForwardGain q r

Representative-only corollary for the maximal-X fiber of each (N,Y) class. The 1/8 gain is the one in (5.87)/(5.91), not the outer exponent θ = 1/20 in (5.76). The constant is exactly the eighth root of the comparison factor 2.