Mixed skipped single-scale bounds

This file isolates the three numerical estimates used in (5.93)--(5.98). The hypothesis RNDominance K R c is the honest local form of R / N ≳ X Y: it says N * X * Y ≤ K * R, with the comparison constant visible. MixedScaleCertificate is the interface expected from Stage 1.

The analytic estimates below deliberately use the stronger threshold max a.N b.N on the second edge. This is what permits the summation order to be chosen in the left-skipped/right-unskipped case, as in the paper.

def Anderson4D.XYCluster.RNDominance (K R : ℝ) (c : XYCluster) : Prop

The explicit, constant-carrying version of R / N ≳ X Y.

Equations

• Anderson4D.XYCluster.RNDominance K R c = (c.N * c.X * c.Y ≤ K * R)

noncomputable def Anderson4D.XYCluster.forwardGain (a b : XYCluster) : ℝ

The gain on the right-hand side of (5.91).

Equations

• a.forwardGain b = min 1 ((b.P / a.P) ^ (1 / 8))

noncomputable def Anderson4D.XYCluster.reverseGain (a b : XYCluster) : ℝ

The reciprocal gain appearing in (5.93), (5.96), and (5.98).

Equations

• a.reverseGain b = max 1 ((a.P / b.P) ^ (1 / 8))

noncomputable def Anderson4D.XYCluster.skipXi (c : XYCluster) (skipped : Bool) : ℝ

The factor Ξ from (5.91).

Equations

• c.skipXi skipped = if skipped = true then (√(c.X * c.Y))⁻¹ else 1

noncomputable def Anderson4D.XYCluster.strongLambda (a b : XYCluster) (R : ℝ) (skipped : Bool) (x y : Fin 4 → ℤ) : ℝ

The second edge, with the scale cutoff required in the mixed cases.

Equations

• a.strongLambda b R skipped x y = if skipped = true then R⁻¹ ^ 2 else if max a.N b.N ≤ Anderson4D.znorm (x - y) then (Anderson4D.znorm (x - y))⁻¹ ^ 2 else 0

noncomputable def Anderson4D.XYCluster.mixedPairInner (a b : XYCluster) (R : ℝ) (skipA skipB : Bool) (u : Fin 4 → ℤ) : ℝ

The two-edge local sum whose four skip cases are assembled below.

Equations

• a.mixedPairInner b R skipA skipB u = a.X * b.X * ∑ x ∈ a.points, a.lambda R skipA u x * ∑ y ∈ b.points, a.strongLambda b R skipB x y

noncomputable def Anderson4D.XYCluster.mixedTarget (a b : XYCluster) (skipA skipB : Bool) : ℝ

The right-hand side of (5.91), before its universal constant.

Equations

• a.mixedTarget b skipA skipB = a.X * √a.Y * a.N⁻¹ ^ 2 * (b.X * √b.Y * b.N⁻¹ ^ 2) * a.skipXi skipA * b.skipXi skipB * a.forwardGain b

def Anderson4D.XYCluster.Line593 (K R : ℝ) (a b : XYCluster) : Prop

The numerical condition displayed in (5.93), with constant K.

Equations

• Anderson4D.XYCluster.Line593 K R a b = (√a.X * a.Y * (√b.X * b.Y) * a.reverseGain b ≤ K * ((R / a.N) ^ 2 * (R / b.N) ^ 2))

def Anderson4D.XYCluster.Line596 (K R : ℝ) (a b : XYCluster) : Prop

The numerical condition displayed in (5.96), with constant K.

Equations

• Anderson4D.XYCluster.Line596 K R a b = (√b.X * b.Y * a.reverseGain b ≤ K * (R / b.N) ^ 2)

def Anderson4D.XYCluster.Line598 (K R : ℝ) (a b : XYCluster) : Prop

The numerical condition displayed in (5.98), with constant K.

Equations

• Anderson4D.XYCluster.Line598 K R a b = (√(a.X * a.Y) * max √a.Y √b.Y * a.reverseGain b ≤ K * (R / min a.N b.N) ^ 2)

structure Anderson4D.XYCluster.MixedScaleCertificate (Kdom Knum R : ℝ) (a b : XYCluster) : Prop

Stage 1's explicit interface to the mixed-case proof.

The first two fields record the genuine input N X Y ≤ Kdom R; the final three fields are the numerical consequences (5.93), (5.96), and (5.98). Keeping both is intentional: it prevents a later stage from silently treating separation as if it implied the required mass domination.

• a_dominance : RNDominance Kdom R a
• b_dominance : RNDominance Kdom R b
• line593 : Line593 Knum R a b
• line596 : Line596 Knum R a b
• line598 : Line598 Knum R a b

theorem Anderson4D.XYCluster.Y_pos_of_nonempty {c : XYCluster} (hc : c.points.Nonempty) : 0 < c.Y

theorem Anderson4D.XYCluster.P_pos_of_nonempty {c : XYCluster} (hc : c.points.Nonempty) : 0 < c.P

theorem Anderson4D.XYCluster.P_nonneg' (c : XYCluster) : 0 ≤ c.P

theorem Anderson4D.XYCluster.one_le_Y_of_nonempty {c : XYCluster} (hc : c.points.Nonempty) : 1 ≤ c.Y

theorem Anderson4D.XYCluster.mass_le_R_div_N {R : ℝ} {c : XYCluster} (hdom : RNDominance 1 R c) : c.X * c.Y ≤ R / c.N

theorem Anderson4D.XYCluster.line593_of_dominance_one {R : ℝ} {a b : XYCluster} (haX : 1 ≤ a.X) (hbX : 1 ≤ b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hda : RNDominance 1 R a) (hdb : RNDominance 1 R b) : Line593 1 R a b

theorem Anderson4D.XYCluster.line596_of_dominance_one {R : ℝ} {a b : XYCluster} (haX : 1 ≤ a.X) (hbX : 1 ≤ b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hda : RNDominance 1 R a) (hdb : RNDominance 1 R b) : Line596 1 R a b

theorem Anderson4D.XYCluster.line598_of_dominance_one {R : ℝ} {a b : XYCluster} (haX : 1 ≤ a.X) (hbX : 1 ≤ b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hda : RNDominance 1 R a) (hdb : RNDominance 1 R b) : Line598 1 R a b

theorem Anderson4D.XYCluster.mixedScaleCertificate_of_dominance_one {R : ℝ} {a b : XYCluster} (haX : 1 ≤ a.X) (hbX : 1 ≤ b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hda : RNDominance 1 R a) (hdb : RNDominance 1 R b) : MixedScaleCertificate 1 1 R a b

Direct constructor from the exact constant-one Stage-1 mass bounds.

theorem Anderson4D.XYCluster.mixedScaleCertificate_of_dominance_two {R : ℝ} {a b : XYCluster} (haX : 1 ≤ a.X) (hbX : 1 ≤ b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hda : RNDominance 2 R a) (hdb : RNDominance 2 R b) : MixedScaleCertificate 2 16 R a b

Constant-carrying constructor used by the single-scale assembly.

The dyadic bucket has fewer than twice its recorded Y points, so the root-scale budget naturally supplies RNDominance 2 R. Viewing this as constant-one dominance at radius 2 * R gives factors 16, 4, and 4 in (5.93), (5.96), and (5.98), respectively; the latter two are enlarged to the common numerical constant 16.

theorem Anderson4D.XYCluster.forwardGain_nonneg (a b : XYCluster) : 0 ≤ a.forwardGain b

theorem Anderson4D.XYCluster.reverseGain_one_le (a b : XYCluster) : 1 ≤ a.reverseGain b

theorem Anderson4D.XYCluster.forwardGain_mul_reverseGain {a b : XYCluster} (ha : a.points.Nonempty) (hb : b.points.Nonempty) : a.forwardGain b * a.reverseGain b = 1

theorem Anderson4D.XYCluster.mixedPairInner_le_unskipped : ∃ (C : ℝ), 0 < C ∧ ∀ (a b : XYCluster) (R : ℝ) (u : Fin 4 → ℤ), a.mixedPairInner b R false false u ≤ C * a.mixedTarget b false false

The false/false branch of (5.91), directly from Lemma 5.14.

theorem Anderson4D.XYCluster.mixedPairInner_bothSkipped (a b : XYCluster) (R : ℝ) (u : Fin 4 → ℤ) : a.mixedPairInner b R true true u = a.X * b.X * a.Y * b.Y * R⁻¹ ^ 4

Exact rough value in the both-skipped branch, the left side of (5.93).

theorem Anderson4D.XYCluster.mixedPairInner_rightSkipped_rough : ∃ (C : ℝ), 0 < C ∧ ∀ (a b : XYCluster) (R : ℝ) (u : Fin 4 → ℤ), a.mixedPairInner b R false true u ≤ C * (a.X * √a.Y * a.N⁻¹ ^ 2) * (b.X * b.Y * R⁻¹ ^ 2)

The analytic summation used before applying the numerical condition (5.96).

theorem Anderson4D.XYCluster.mixedPairInner_leftSkipped_rough : ∃ (C : ℝ), 0 < C ∧ ∀ (a b : XYCluster) (R : ℝ) (u : Fin 4 → ℤ), a.mixedPairInner b R true false u ≤ C * a.X * b.X * R⁻¹ ^ 2 * if a.N ≤ b.N then a.Y * √b.Y * b.N⁻¹ ^ 2 else b.Y * √a.Y * a.N⁻¹ ^ 2

The analytic summation used before (5.98). The branch records exactly the paper's instruction to sum the variable belonging to the larger scale.

theorem Anderson4D.XYCluster.bothSkipped_le_of_line593 {K R : ℝ} {a b : XYCluster} (haX : 0 < a.X) (hbX : 0 < b.X) (ha : a.points.Nonempty) (hb : b.points.Nonempty) (hR : 0 < R) (h593 : Line593 K R a b) (u : Fin 4 → ℤ) : a.mixedPairInner b R true true u ≤ K * a.mixedTarget b true true

theorem Anderson4D.XYCluster.mixedPairInner_rightSkipped_le : ∃ (C : ℝ), 0 < C ∧ ∀ (K R : ℝ) (a b : XYCluster) (u : Fin 4 → ℤ), a.points.Nonempty → b.points.Nonempty → 0 < b.X → 0 < R → Line596 K R a b → a.mixedPairInner b R false true u ≤ C * K * a.mixedTarget b false true

The false/true branch of (5.91), using precisely the sufficient condition (5.96).

theorem Anderson4D.XYCluster.mixedPairInner_leftSkipped_le : ∃ (C : ℝ), 0 < C ∧ ∀ (K R : ℝ) (a b : XYCluster) (u : Fin 4 → ℤ), a.points.Nonempty → b.points.Nonempty → 0 < a.X → 0 < R → Line598 K R a b → a.mixedPairInner b R true false u ≤ C * K * a.mixedTarget b true false

The true/false branch of (5.91), with the two summation orders in (5.98).

theorem Anderson4D.XYCluster.mixedTarget_nonneg (a b : XYCluster) (skipA skipB : Bool) : 0 ≤ a.mixedTarget b skipA skipB

theorem Anderson4D.XYCluster.mixedPairInner_le_5_91 : ∃ (C : ℝ), 0 < C ∧ ∀ (Kdom Knum R : ℝ) (a b : XYCluster) (skipA skipB : Bool) (u : Fin 4 → ℤ), 0 ≤ Knum → 1 ≤ a.X → 1 ≤ b.X → a.points.Nonempty → b.points.Nonempty → 0 < R → MixedScaleCertificate Kdom Knum R a b → a.mixedPairInner b R skipA skipB u ≤ C * max 1 Knum * a.mixedTarget b skipA skipB

Uniform local bound (5.91), ready for the parity assembly.

Kdom is carried only by the explicit Stage-1 dominance fields of cert; Knum is the constant in the three numerical consequences (5.93), (5.96), and (5.98). Thus the conclusion never hides a comparison constant.

theorem Anderson4D.XYCluster.mixedPairInner_le_5_91_of_dominance_one : ∃ (C : ℝ), 0 < C ∧ ∀ (R : ℝ) (a b : XYCluster) (skipA skipB : Bool) (u : Fin 4 → ℤ), 1 ≤ a.X → 1 ≤ b.X → a.points.Nonempty → b.points.Nonempty → RNDominance 1 R a → RNDominance 1 R b → a.mixedPairInner b R skipA skipB u ≤ C * a.mixedTarget b skipA skipB

Normalized constant-one convenience form of the local estimate.

The actual dyadic-bucket assembly uses mixedPairInner_le_5_91_of_dominance_two below, because the cluster stores the actual point-cardinality while the setup budget stores its dyadic floor.

theorem Anderson4D.XYCluster.mixedPairInner_le_5_91_of_dominance_two : ∃ (C : ℝ), 0 < C ∧ ∀ (R : ℝ) (a b : XYCluster) (skipA skipB : Bool) (u : Fin 4 → ℤ), 1 ≤ a.X → 1 ≤ b.X → a.points.Nonempty → b.points.Nonempty → RNDominance 2 R a → RNDominance 2 R b → a.mixedPairInner b R skipA skipB u ≤ C * a.mixedTarget b skipA skipB

Assembly-facing form of (5.91).

The factor 2 in the root-scale dominance accounts for replacing the dyadic bucket size by the actual number of points. The induced numerical constant 16 is absorbed into the universal constant in the conclusion.