Single-scale proof setup

This file implements Steps 1--2 of the proof of Proposition 5.10: the power count (5.68) and the finite dyadic classification (5.74)--(5.75).

Step 1: the exact excess identity (5.68)

theorem Anderson4D.sum_gammaInf_sub_one_eq_totalMultiplicity_sub_one {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) : ∑ v ∈ t.BranchNodes, (gammaInf mu v - 1) = totalMultiplicity mu - 1

Paper equation (5.68), with m unfolded as totalMultiplicity.

theorem Anderson4D.gammaInf_le_two_mul_sub_one {t : PlaneTree} (mu : t.Multiplicities) {v : t.VPos} (hv : v ∈ t.BranchNodes) : gammaInf mu v ≤ 2 * (gammaInf mu v - 1)

Pointwise inequality used after (5.68) to absorb the exponential in (5.69): γ∞ ≤ 2(γ∞-1) at every branch node.

theorem Anderson4D.sum_gammaInf_le_two_mul_totalMultiplicity_sub_one {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) : ∑ v ∈ t.BranchNodes, gammaInf mu v ≤ 2 * (totalMultiplicity mu - 1)

Summed power-count consequence of (5.68), with the constant in (5.69) made explicit.

Corrected exponential cost in (5.69)

As recorded in docs/PAPER_NOTES.md (5.69), the inclusive ancestor sum contains the self term. Its uniform bound is 2, not the displayed 1; this leaves the paper's final C^m estimate unchanged.

def Anderson4D.weakNonrootBranchAncestors {t : PlaneTree} (u : t.VPos) : Finset t.VPos

Equations

• Anderson4D.weakNonrootBranchAncestors u = {n ∈ Anderson4D.nonrootBranches t | ↑n <+: ↑u}

theorem Anderson4D.sum_weakNonrootAncestor_ratios_le_two {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) {u : t.VPos} (hu : u ∈ t.BranchNodes) : ∑ n ∈ weakNonrootBranchAncestors u, ↑(scaleN Nm u) / ↑(scaleN Nm n) ≤ 2

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

The exponent in the product-to-exponential step of (5.69), before reordering the two finite sums.

Equations

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

theorem Anderson4D.sum_accumulatedScale_div_eq_exponentCost {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ∑ n ∈ nonrootBranches t, ↑(accumulatedScale Nm mu n) / ↑(scaleN Nm n) = singleScaleExponentCost Nm mu

singleScaleExponentCost is exactly the sum of the normalized accumulated scales occurring after x ≤ exp x in (5.69).

theorem Anderson4D.singleScaleExponentCost_eq_reordered {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : singleScaleExponentCost Nm mu = ∑ u ∈ t.BranchNodes, ↑(gammaInf mu u) * ∑ n ∈ weakNonrootBranchAncestors u, ↑(scaleN Nm u) / ↑(scaleN Nm n)

theorem Anderson4D.singleScaleExponentCost_le_two_sum_gammaInf {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) : singleScaleExponentCost Nm mu ≤ 2 * ∑ u ∈ t.BranchNodes, ↑(gammaInf mu u)

Quantitative core of the local constant adjustment in (5.69): the reordered exponent costs at most twice ∑γ∞.

theorem Anderson4D.singleScaleExponentCost_le_four_mul_total_sub_one {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) : singleScaleExponentCost Nm mu ≤ 4 * ↑(totalMultiplicity mu - 1)

Combining the local (5.69) constant adjustment with (5.68) gives the explicit exponent 4(m-1).

Step 2: the (N,X,Y,P) classification (5.74)

theorem Anderson4D.parentScale_separation {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) {l l' : HeppLeaf t} (hne : l ≠ l') : ↑(max (scaleN Nm (PlaneTree.parentV ↑l)) (scaleN Nm (PlaneTree.parentV ↑l'))) / 2 ≤ znorm (z l - z l')

Paper (5.73): separation at the LCA scale implies separation at half the larger of the two parent scales.

The path correction in the power ledger (5.71)

def Anderson4D.branchChildrenTowardLeaf {t : PlaneTree} (v : t.VPos) (l : HeppLeaf t) : Finset t.VPos

Branch children of v lying on the path to l.

Equations

• Anderson4D.branchChildrenTowardLeaf v l = {c ∈ Anderson4D.branchChildren v | ↑c <+: ↑↑l}

theorem Anderson4D.card_branchChildrenTowardLeaf {t : PlaneTree} (ht : t.isValid = true) {v : t.VPos} (hv : v ∈ t.BranchNodes) (l : HeppLeaf t) : (branchChildrenTowardLeaf v l).card = if ↑v <+: ↑↑l then if v = PlaneTree.parentV ↑l then 0 else 1 else 0

The correction fiber in (5.71) has cardinality zero off the leaf path and at its parent, and cardinality one at every earlier ancestor.

theorem Anderson4D.gamma2_power_count {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) (compound : Finset t.VPos) (v : t.VPos) : gamma2 mu compound v = (branchChildren v).card + 2 * (childrenOf v ∩ simpleLeaves t compound).card + ∑ l ∈ childrenOf v ∩ compoundLeaves t compound, mu.m l

The unsubtracted form of the first nodewise power count below (5.71).

theorem Anderson4D.gamma2_sub_one_power_count {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) (compound : Finset t.VPos) (v : t.VPos) : gamma2 mu compound v - 1 = (branchChildren v).card + 2 * (childrenOf v ∩ simpleLeaves t compound).card + ∑ l ∈ childrenOf v ∩ compoundLeaves t compound, mu.m l - 1

The first line of the nodewise exponent count below (5.71).

def Anderson4D.paper571RhsExponent {t : PlaneTree} (mu : t.Multiplicities) (compound : Finset t.VPos) (l0 : HeppLeaf t) (v : t.VPos) : ℤ

The RHS exponent printed in the second line below (5.71), including the leaf-path correction contributed by the ratio product.

Equations

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

theorem Anderson4D.paper571_exponent_identity {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) (compound : Finset t.VPos) (l0 : HeppLeaf t) {v : t.VPos} (hv : v ∈ t.BranchNodes) : ↑(gamma2 mu compound v) - 1 = paper571RhsExponent mu compound l0 v

Full nodewise exponent identity underlying paper (5.71).

def Anderson4D.dyadicFloor (q : ℕ) : ℕ

Largest power of two not exceeding q (the value at q = 0 is unused).

Equations

• Anderson4D.dyadicFloor q = 2 ^ Nat.log 2 q

theorem Anderson4D.dyadicFloor_bounds {q : ℕ} (hq : q ≠ 0) : dyadicFloor q ≤ q ∧ q < 2 * dyadicFloor q

@[reducible, inline]

abbrev Anderson4D.NXClass : Type

Equations

• Anderson4D.NXClass = (ℕ × ℕ)

@[reducible, inline]

abbrev Anderson4D.NYClass : Type

Equations

• Anderson4D.NYClass = (ℕ × ℕ)

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

σ₁(l) = (N,X): parent scale and multiplicity dyadic block.

Equations

• Anderson4D.singleScaleSigma1 Nm mu l = (Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV ↑l), Anderson4D.dyadicFloor (Anderson4D.leafMultiplicity mu l))

def Anderson4D.leavesAtNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NXClass) : Finset (HeppLeaf t)

The exact leaf fiber L_{N,X}.

Equations

• Anderson4D.leavesAtNX Nm mu q = {l : Anderson4D.HeppLeaf t | Anderson4D.singleScaleSigma1 Nm mu l = q}

def Anderson4D.nxCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Finset NXClass

Only (N,X) blocks which actually occur.

Equations

• Anderson4D.nxCarrier Nm mu = Finset.image (Anderson4D.singleScaleSigma1 Nm mu) Finset.univ

@[reducible, inline]

abbrev Anderson4D.ActiveNXClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

The finite type of active (N,X) classes.

Equations

• Anderson4D.ActiveNXClass Nm mu = ↥(Anderson4D.nxCarrier Nm mu)

def Anderson4D.singleScaleSigma2 {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NXClass) : NYClass

σ₂(N,X) = (N,Y), where Y dyadically brackets |L_{N,X}|.

Equations

• Anderson4D.singleScaleSigma2 Nm mu q = (q.1, Anderson4D.dyadicFloor (Anderson4D.leavesAtNX Nm mu q).card)

def Anderson4D.nyCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Finset NYClass

Only (N,Y) blocks which actually occur.

Equations

• Anderson4D.nyCarrier Nm mu = Finset.image (Anderson4D.singleScaleSigma2 Nm mu) (Anderson4D.nxCarrier Nm mu)

def Anderson4D.singleScaleSigma3 (q : NYClass) : ℕ

σ₃(N,Y) = P = YN⁴.

Equations

• Anderson4D.singleScaleSigma3 q = q.2 * q.1 ^ 4

def Anderson4D.pCarrier {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Finset ℕ

Only volume parameters P which actually occur.

Equations

• Anderson4D.pCarrier Nm mu = Finset.image Anderson4D.singleScaleSigma3 (Anderson4D.nyCarrier Nm mu)

@[reducible, inline]

abbrev Anderson4D.ActivePClass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

The finite type of distinct active values P = Y N⁴.

Equations

• Anderson4D.ActivePClass Nm mu = ↥(Anderson4D.pCarrier Nm mu)

def Anderson4D.nxAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : Finset NXClass

Equations

• Anderson4D.nxAtNY Nm mu q = {a ∈ Anderson4D.nxCarrier Nm mu | Anderson4D.singleScaleSigma2 Nm mu a = q}

def Anderson4D.nyAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Finset NYClass

Equations

• Anderson4D.nyAtP Nm mu P = {q ∈ Anderson4D.nyCarrier Nm mu | Anderson4D.singleScaleSigma3 q = P}

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

The exact leaf carrier L_{N,Y} induced by σ₂ ∘ σ₁.

Equations

• Anderson4D.leavesAtNY Nm mu q = {l : Anderson4D.HeppLeaf t | Anderson4D.singleScaleSigma2 Nm mu (Anderson4D.singleScaleSigma1 Nm mu l) = q}

def Anderson4D.leavesAtP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : Finset (HeppLeaf t)

The exact leaf carrier L_P induced by σ₃ ∘ σ₂ ∘ σ₁.

Equations

• Anderson4D.leavesAtP Nm mu P = {l : Anderson4D.HeppLeaf t | Anderson4D.singleScaleSigma3 (Anderson4D.singleScaleSigma2 Nm mu (Anderson4D.singleScaleSigma1 Nm mu l)) = P}

def Anderson4D.maxXAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : ℕ

The paper's maximal X* in the σ₂-fiber.

Equations

• Anderson4D.maxXAtNY Nm mu q = (Anderson4D.nxAtNY Nm mu q).sup Prod.snd

theorem Anderson4D.sigma1_bucket {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (l : HeppLeaf t) : (singleScaleSigma1 Nm mu l).2 ≤ leafMultiplicity mu l ∧ leafMultiplicity mu l < 2 * (singleScaleSigma1 Nm mu l).2

theorem Anderson4D.sigma2_bucket {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NXClass} (hq : q ∈ nxCarrier Nm mu) : (singleScaleSigma2 Nm mu q).2 ≤ (leavesAtNX Nm mu q).card ∧ (leavesAtNX Nm mu q).card < 2 * (singleScaleSigma2 Nm mu q).2

theorem Anderson4D.nxClass_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NXClass} (hq : q ∈ nxCarrier Nm mu) : IsDyadicNat q.1 ∧ IsDyadicNat q.2

theorem Anderson4D.nyClass_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : IsDyadicNat q.1 ∧ IsDyadicNat q.2

theorem Anderson4D.pClass_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {P : ℕ} (hP : P ∈ pCarrier Nm mu) : IsDyadicNat P

def Anderson4D.multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NXClass) : ℕ

Equations

• Anderson4D.multiplicityNX Nm mu q = ∑ l ∈ Anderson4D.leavesAtNX Nm mu q, Anderson4D.leafMultiplicity mu l

theorem Anderson4D.multiplicityNX_bounds {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NXClass} (hq : q ∈ nxCarrier Nm mu) : q.2 * (singleScaleSigma2 Nm mu q).2 ≤ multiplicityNX Nm mu q ∧ multiplicityNX Nm mu q < 4 * q.2 * (singleScaleSigma2 Nm mu q).2

Quantitative form of m_{N,X} ∼ XY in (5.75), with constants 1,4.

theorem Anderson4D.nxClass_second_eq_pow_log {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NXClass} (hq : q ∈ nxCarrier Nm mu) : q.2 = 2 ^ Nat.log 2 q.2

theorem Anderson4D.sum_X_nxAtNY_le_two_maxX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : ∑ a ∈ nxAtNY Nm mu q, a.2 ≤ 2 * maxXAtNY Nm mu q

The distinct dyadic X values in a fixed (N,Y) fiber sum to at most twice their maximum.

The exact finite ledgers in (5.75)

def Anderson4D.multiplicityNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : ℕ

Equations

• Anderson4D.multiplicityNY Nm mu q = ∑ a ∈ Anderson4D.nxAtNY Nm mu q, Anderson4D.multiplicityNX Nm mu a

def Anderson4D.multiplicityP {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : ℕ

Equations

• Anderson4D.multiplicityP Nm mu P = ∑ q ∈ Anderson4D.nyAtP Nm mu P, Anderson4D.multiplicityNY Nm mu q

theorem Anderson4D.multiplicityNY_bounds {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : maxXAtNY Nm mu q * q.2 ≤ multiplicityNY Nm mu q ∧ multiplicityNY Nm mu q ≤ 8 * maxXAtNY Nm mu q * q.2

Quantitative form of m_{N,Y} ∼ X*Y in (5.75), with constants 1,8.

theorem Anderson4D.multiplicityNY_eq_fiber_sum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : multiplicityNY Nm mu q = ∑ a ∈ nxAtNY Nm mu q, multiplicityNX Nm mu a

m_{N,Y} = ∑_{σ₂(N,X)=(N,Y)} m_{N,X} in (5.75).

theorem Anderson4D.multiplicityP_eq_fiber_sum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : multiplicityP Nm mu P = ∑ q ∈ nyAtP Nm mu P, multiplicityNY Nm mu q

m_P = ∑_{YN⁴=P} m_{N,Y} in (5.75).

theorem Anderson4D.multiplicityNY_eq_leaf_sum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) : multiplicityNY Nm mu q = ∑ l ∈ leavesAtNY Nm mu q, leafMultiplicity mu l

The nested σ₂ ledger is exactly the multiplicity sum on L_{N,Y}.

theorem Anderson4D.multiplicityP_eq_leaf_sum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (P : ℕ) : multiplicityP Nm mu P = ∑ l ∈ leavesAtP Nm mu P, leafMultiplicity mu l

The nested σ₃ ledger is exactly the multiplicity sum on L_P.

theorem Anderson4D.sum_multiplicityNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ∑ q ∈ nxCarrier Nm mu, multiplicityNX Nm mu q = totalMultiplicity mu

theorem Anderson4D.sum_multiplicityNY_eq_sum_NX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ∑ q ∈ nyCarrier Nm mu, multiplicityNY Nm mu q = ∑ a ∈ nxCarrier Nm mu, multiplicityNX Nm mu a

theorem Anderson4D.sum_multiplicityP_eq_sum_NY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ∑ P ∈ pCarrier Nm mu, multiplicityP Nm mu P = ∑ q ∈ nyCarrier Nm mu, multiplicityNY Nm mu q

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

The final identity m = ∑_P m_P in (5.75).

Root-scale budget used by the mixed skipped-edge estimate

def Anderson4D.weightedLeafMass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : ℕ

Equations

• Anderson4D.weightedLeafMass Nm mu = ∑ l : Anderson4D.HeppLeaf t, Anderson4D.leafMultiplicity mu l * Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV ↑l)

@[simp]

theorem Anderson4D.branchNodesUnder_root (t : PlaneTree) : branchNodesUnder t.rootV = t.BranchNodes

theorem Anderson4D.weightedLeafMass_le_accumulatedRoot {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) : weightedLeafMass Nm mu ≤ accumulatedScale Nm mu t.rootV

The exact global budget behind R/N ≳ X*Y: all leaf mass weighted by its parent scale is bounded by the root accumulated scale.

theorem Anderson4D.nxScale_mul_multiplicity_le_weightedLeafMass {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NXClass) : q.1 * multiplicityNX Nm mu q ≤ weightedLeafMass Nm mu

One (N,X) block consumes at least N m_{N,X} of the global leaf budget. This exact inequality is the bridge from classification to R.

theorem Anderson4D.nyClass_scale_mul_Y_mul_maxX_le_R {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : q.1 * q.2 * maxXAtNY Nm mu q ≤ R

Explicit form of the paper's R/N ≳ X*Y, used in (5.91): for every active (N,Y) class, N·Y·X* ≤ R with constant exactly one.

theorem Anderson4D.nyClass_Y_mul_maxX_le_R_div_scale {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℕ) (hR : accumulatedScale Nm mu t.rootV ≤ R) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : ↑q.2 * ↑(maxXAtNY Nm mu q) ≤ ↑R / ↑q.1

Division form consumed by the mixed-edge local estimate: X*Y ≤ R/N.

Interface to the analytic XYCluster estimates

An (N,Y) class can contain several (N,X) fibers. The point set used by Lemma 5.14 is one such (N,X) fiber, not their union. For the coarse (N,Y) interface we canonically choose a fiber attaining X*.

theorem Anderson4D.nxAtNY_nonempty {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : (nxAtNY Nm mu q).Nonempty

noncomputable def Anderson4D.maxNXAtNY {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : NXClass

A canonical (N,X*) representative of an active (N,Y) class.

Equations

• Anderson4D.maxNXAtNY Nm mu q hq = Classical.choose ⋯

theorem Anderson4D.maxNXAtNY_mem {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : maxNXAtNY Nm mu q hq ∈ nxAtNY Nm mu q

@[simp]

theorem Anderson4D.maxNXAtNY_snd {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : (maxNXAtNY Nm mu q hq).2 = maxXAtNY Nm mu q

@[simp]

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

theorem Anderson4D.maxNXAtNY_active {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : maxNXAtNY Nm mu q hq ∈ nxCarrier Nm mu

theorem Anderson4D.leavesAtNX_nonempty {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : (leavesAtNX Nm mu a).Nonempty

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

theorem Anderson4D.two_le_nxClass_scale {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : 2 ≤ a.1

noncomputable def Anderson4D.nxClassNhat (a : NXClass) : ℝ

The actual lattice scale supplied to Lemma 5.14. The factor 1/2 is exactly the separation loss in (5.73).

Equations

• Anderson4D.nxClassNhat a = max 1 (↑a.1 / 2)

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

Embedded point set of one active (N,X) fiber.

Equations

• Anderson4D.nxClassPoints Nm mu z a = Finset.image z (Anderson4D.leavesAtNX Nm mu a)

theorem Anderson4D.nxClassNhat_eq_half {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : nxClassNhat a = ↑a.1 / 2

theorem Anderson4D.nxClassPoints_nonempty {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) : (nxClassPoints Nm mu z a).Nonempty

theorem Anderson4D.card_nxClassPoints {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : Function.Injective z) (a : NXClass) : (nxClassPoints Nm mu z a).card = (leavesAtNX Nm mu a).card

theorem Anderson4D.nxClassPoints_separated {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) (x : Fin 4 → ℤ) : x ∈ nxClassPoints Nm mu z a → ∀ y ∈ nxClassPoints Nm mu z a, x ≠ y → nxClassNhat a ≤ znorm (x - y)

noncomputable def Anderson4D.nxClassCluster {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) : XYCluster

Paper-facing analytic cluster attached to one active (N,X) fiber.

Equations

• Anderson4D.nxClassCluster ht hroot Nm mu z hz a ha = { points := Anderson4D.nxClassPoints Nm mu z a, X := ↑a.2, N := Anderson4D.nxClassNhat a, X_nonneg := ⋯, one_le_N := ⋯, separated := ⋯ }

noncomputable def Anderson4D.nyClassCluster {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) : XYCluster

The (N,Y) coarse representative is its canonical maximal-X fiber.

Equations

• Anderson4D.nyClassCluster ht hroot Nm mu z hz q hq = Anderson4D.nxClassCluster ht hroot Nm mu z hz (Anderson4D.maxNXAtNY Nm mu q hq) ⋯

@[simp]

theorem Anderson4D.nxClassCluster_points {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 = nxClassPoints Nm mu z a

@[simp]

theorem Anderson4D.nxClassCluster_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) : (nxClassCluster ht hroot Nm mu z hz a ha).X = ↑a.2

@[simp]

theorem Anderson4D.nxClassCluster_N {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).N = ↑a.1 / 2

theorem Anderson4D.nxClassCluster_card_bounds {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) : (singleScaleSigma2 Nm mu a).2 ≤ (nxClassCluster ht hroot Nm mu z hz a ha).points.card ∧ (nxClassCluster ht hroot Nm mu z hz a ha).points.card < 2 * (singleScaleSigma2 Nm mu a).2

theorem Anderson4D.nxClass_X_mul_card_le_multiplicity {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : a.2 * (leavesAtNX Nm mu a).card ≤ multiplicityNX Nm mu a

theorem Anderson4D.nxClassCluster_R_dominance_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) : (nxClassCluster ht hroot Nm mu z hz a ha).N * (nxClassCluster ht hroot Nm mu z hz a ha).X * (nxClassCluster ht hroot Nm mu z hz a ha).Y ≤ ↑R

The exact raw form of the root-budget hypothesis needed by the mixed analytic estimate, for any active (N,X) fiber.

theorem Anderson4D.nxClassCluster_P_lower {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) : ↑(singleScaleSigma3 (singleScaleSigma2 Nm mu a)) ≤ 16 * (nxClassCluster ht hroot Nm mu z hz a ha).P

The dyadic proxy YN⁴ and the actual Lemma 5.14 volume |L_{N,X}|(N/2)⁴ differ by fixed constants only.

theorem Anderson4D.nxClassCluster_P_upper {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) : 8 * (nxClassCluster ht hroot Nm mu z hz a ha).P ≤ ↑(singleScaleSigma3 (singleScaleSigma2 Nm mu a))

@[simp]

theorem Anderson4D.nyClassCluster_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) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : (nyClassCluster ht hroot Nm mu z hz q hq).X = ↑(maxXAtNY Nm mu q)

@[simp]

theorem Anderson4D.nyClassCluster_N {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) : (nyClassCluster ht hroot Nm mu z hz q hq).N = ↑q.1 / 2

theorem Anderson4D.nyClassCluster_one_le_N {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) : 1 ≤ (nyClassCluster ht hroot Nm mu z hz q hq).N

theorem Anderson4D.nyClassCluster_separated {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) (x : Fin 4 → ℤ) : x ∈ (nyClassCluster ht hroot Nm mu z hz q hq).points → ∀ y ∈ (nyClassCluster ht hroot Nm mu z hz q hq).points, x ≠ y → (nyClassCluster ht hroot Nm mu z hz q hq).N ≤ znorm (x - y)

theorem Anderson4D.nyClassCluster_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) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : (nyClassCluster ht hroot Nm mu z hz q hq).points.Nonempty

theorem Anderson4D.nyClassCluster_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) (q : NYClass) (hq : q ∈ nyCarrier Nm mu) : 1 ≤ (nyClassCluster ht hroot Nm mu z hz q hq).X

theorem Anderson4D.nyClassCluster_card_bounds {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) : q.2 ≤ (nyClassCluster ht hroot Nm mu z hz q hq).points.card ∧ (nyClassCluster ht hroot Nm mu z hz q hq).points.card < 2 * q.2

theorem Anderson4D.nyClassCluster_R_dominance_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) : (nyClassCluster ht hroot Nm mu z hz q hq).N * (nyClassCluster ht hroot Nm mu z hz q hq).X * (nyClassCluster ht hroot Nm mu z hz q hq).Y ≤ 2 * ↑R

The requested setup-side bridge. SingleScaleMixed can turn this definition-free inequality into RNDominance 2 R by one simplification.

theorem Anderson4D.nyClass_P_dyadic {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {q : NYClass} (hq : q ∈ nyCarrier Nm mu) : IsDyadicNat (singleScaleSigma3 q)

theorem Anderson4D.nyClassCluster_P_comparable {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) : 8 * (nyClassCluster ht hroot Nm mu z hz q hq).P ≤ ↑(singleScaleSigma3 q) ∧ ↑(singleScaleSigma3 q) ≤ 16 * (nyClassCluster ht hroot Nm mu z hz q hq).P

Constant comparison needed to replace the analytic cluster's actual P = |points| N̂⁴ by the paper's dyadic P = YN⁴.