Paper §4.2, Steps 2 and 3: the second moment

Paper: R-324 — §4.2 Steps 2–3 — interval structure, positional count, nested chain

This file transcribes Steps 2 and 3 of Section 4.2 of arXiv:2607.10105v1 (pages 19–20) literally, in the paper's own order, continuing R324PaperStep1 (Step 1).

Step 2.

• r324Step2_wick_regroup — (a) by Wick, summing over (κ₊, κ₋, π) is summing over full pairings κ′ of [1, 2m].
• isRelFullyPaired_univ_iff — (b) Definition 3.1 / Proposition 3.2 at the start of the extraction.
• card_intervalConfigs_le, card_intervalConfigs_two_mul_le — (c) "we may fix the positions of these subintervals at O(C^m) cost", with C = 16. This is the entire combinatorial cost of §4.2, and it is a purely positional count.
• (d)–(f) — (4.18), the successive removal of each I_i gaining Cλ and introducing H with |H| ≲ |z|⁻², and only then taking absolute values to reach (4.19) — are the §4.1 iteration, recorded as the single named hypothesis R324Step23Reduction (exactly as R324Step1Reduction records it for Step 1).

Step 3.

• r324Step3_external_legs — (a) integrating in (x, y, z, w) yields constants, giving (4.20).
• r324Step3_fullyPaired_straddles, r324Step3_strict_nested — (b) the key structural lemma: since the pairing κ₀ induces on [1, p] and on [p+1, p+q] is primitive and not full, every fully paired subinterval contains {p, p+1}, and any two of them are equal or strictly nested. This is the paper's 1 ≤ a_t < ⋯ < a₁ ≤ p < p+1 ≤ b₁ < ⋯ < b_t ≤ p+q, and it is what replaces every form of grading or per-contraction budget.
• exists_r324Step3_elementaryEightDim_le — (c) the elementary eight-dimensional integral that removes [a₁, b₁] and reassembles the structure of (4.20).
• r324Step3_chain_induction — (d) the induction along the nested chain.
• r324Step23_output_identity, exists_r324Step23_bound — the last line, (Cλ)^{2m}|log ε|⁻¹ ≤ λ_ε² · C (Cλ)^{2m-2}, i.e. (3.24) with 1 on the right, in the form used by the downstream estimates.

Every analytic input is a proved theorem: momentContractionEquivFullPairing (the Wick regrouping), exists_r324ProperInsertedConvolution_le (the elementary eight-dimensional integral), integral_invSqKer_sub_left (the external legs) and exists_integral_primitiveInsertedMajorant_le (the last application of (4.4)).

Step 2(a): Wick — the (κ₊, κ₋, π) sum is a full-pairing sum

theorem Anderson4D.r324Step2_wick_regroup {m : ℕ} {A : Type u_1} [AddCommMonoid A] (F : PartialPairing (Fin (2 * m)) → A) : ∑ κp : PartialPairing (Fin m), ∑ κm : PartialPairing (Fin m), ∑ π : ↥κp.singles ≃ ↥κm.singles, F (momentCombinedPairing κp κm π) = ∑ κ : { κ : PartialPairing (Fin (2 * m)) // κ.IsFull }, F ↑κ

Step 2(a). "Summing over (κ₊, κ₋, π) is equivalent to summing over full pairings κ′ of [1, 2m], where κ′ = κ₊ ∪ κ₋ ∪ (∪_i {i, π(i)})." The gluing map is momentCombinedPairing and the equivalence is momentContractionEquivFullPairing.

Step 2(c): fixing the positions of the subintervals costs O(C^m)

The paper: "we may fix the positions of these subintervals at O(C^m) cost". This is a purely positional count. The blocks Ĩ_i that (4.18) positions are pairwise disjoint subintervals of [1, 2m] — that is exactly what the variable product ∏_{j ∈ Ĩ_0} dx_j · ∏_i ∏_{j ∈ Ĩ_i} dx_j of (4.18) asserts — and the number of such configurations is at most 4^{2m} = 16^m. Nothing about pairings or permutations enters: the count below is a statement about positions only.

def Anderson4D.IsIntervalConfig {N : ℕ} (F : Finset (Fin N × Fin N)) : Prop

A positional configuration: a finite family of pairwise disjoint nonempty subintervals of [1, N], each recorded by its endpoint pair (ℓ_i, r_i).

Equations

• Anderson4D.IsIntervalConfig F = ((∀ p ∈ F, p.1 ≤ p.2) ∧ ∀ p ∈ F, ∀ q ∈ F, p ≠ q → Disjoint (Finset.Icc p.1 p.2) (Finset.Icc q.1 q.2))

@[implicit_reducible]

instance Anderson4D.instDecidableIsIntervalConfig {N : ℕ} (F : Finset (Fin N × Fin N)) : Decidable (IsIntervalConfig F)

Equations

• Anderson4D.instDecidableIsIntervalConfig F = decidable_of_iff ((∀ p ∈ F, p.1 ≤ p.2) ∧ ∀ p ∈ F, ∀ q ∈ F, p ≠ q → Disjoint (Finset.Icc p.1 p.2) (Finset.Icc q.1 q.2)) ⋯

def Anderson4D.intervalConfigs (N : ℕ) : Finset (Finset (Fin N × Fin N))

All positional configurations inside [1, N].

Equations

• Anderson4D.intervalConfigs N = {F : Finset (Fin N × Fin N) | Anderson4D.IsIntervalConfig F}

@[simp]

theorem Anderson4D.mem_intervalConfigs {N : ℕ} {F : Finset (Fin N × Fin N)} : F ∈ intervalConfigs N ↔ IsIntervalConfig F

theorem Anderson4D.intervalConfig_eq_of_images {N : ℕ} {F F' : Finset (Fin N × Fin N)} (hF : IsIntervalConfig F) (hF' : IsIntervalConfig F') (hl : Finset.image Prod.fst F = Finset.image Prod.fst F') (hr : Finset.image Prod.snd F = Finset.image Prod.snd F') : F = F'

A positional configuration is determined by its set of left endpoints together with its set of right endpoints.

theorem Anderson4D.card_intervalConfigs_le (N : ℕ) : (intervalConfigs N).card ≤ 4 ^ N

Step 2(c), the positional count. There are at most 4^N configurations of pairwise disjoint subintervals of [1, N].

theorem Anderson4D.card_intervalConfigs_two_mul_le (m : ℕ) : (intervalConfigs (2 * m)).card ≤ 16 ^ m

Step 2(c) at the doubled carrier. Inside [1, 2m] the positional cost is C^m with C = 16; this is the paper's O(C^m), and it is the entire combinatorial cost of §4.2.

Step 2(b): Definition 3.1 at the start of the extraction

Before any removal the Def 3.1 relative notion IsRelFullyPaired κ univ a b of "fully paired subinterval" (Combinatorics/PairingExtract) is the absolute notion IsFullyPairedOn κ (Finset.Icc a b) used throughout Step 3.

theorem Anderson4D.isRelFullyPaired_univ_iff {m : ℕ} {κ : PartialPairing (Fin m)} (a b : Fin m) : IsRelFullyPaired κ Finset.univ a b ↔ a ≤ b ∧ IsFullyPairedOn κ (Finset.Icc a b)

Step 2(b). Definition 3.1's fully paired subintervals of the full index range are exactly the fully paired Finset.Icc a b.

Step 3(b): the key structural lemma — the surviving intervals are nested

After Step 2 the remaining variables are {x_1, …, x_p} (from the left copy) and {x_{p+1}, …, x_{p+q}} (from the right copy), carrying the pairing κ₀. "By our construction, the partial pairing that κ₀ induces on [1, p] and on [p+1, p+q] must both be primitive and not full."

r324SplitBlockLeft / r324SplitBlockRight are the two blocks and R324SidePrimitiveNotFull is the paper's hypothesis on each of them.

def Anderson4D.r324SplitBlockLeft (n p : ℕ) : Finset (Fin n)

The left block [1, p] of the split index set [1, p+q].

Equations

• Anderson4D.r324SplitBlockLeft n p = {i : Fin n | ↑i < p}

def Anderson4D.r324SplitBlockRight (n p : ℕ) : Finset (Fin n)

The right block [p+1, p+q] of the split index set [1, p+q].

Equations

• Anderson4D.r324SplitBlockRight n p = {i : Fin n | p ≤ ↑i}

@[simp]

theorem Anderson4D.mem_r324SplitBlockLeft {n p : ℕ} {i : Fin n} : i ∈ r324SplitBlockLeft n p ↔ ↑i < p

@[simp]

theorem Anderson4D.mem_r324SplitBlockRight {n p : ℕ} {i : Fin n} : i ∈ r324SplitBlockRight n p ↔ p ≤ ↑i

def Anderson4D.R324SidePrimitiveNotFull {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) : Prop

The paper's hypothesis on each half. The pairing induced by κ on the block B is primitive (every fully paired subinterval of B is all of B) and not full (B itself is not fully paired).

Equations

• Anderson4D.R324SidePrimitiveNotFull κ B = ((∀ (a b : Fin n), a ≤ b → Finset.Icc a b ⊆ B → Anderson4D.IsFullyPairedOn κ (Finset.Icc a b) → Finset.Icc a b = B) ∧ ¬Anderson4D.IsFullyPairedOn κ B)

theorem Anderson4D.R324SidePrimitiveNotFull.not_isFullyPairedOn {n : ℕ} {κ : PartialPairing (Fin n)} {B : Finset (Fin n)} (h : R324SidePrimitiveNotFull κ B) {a b : Fin n} (hab : a ≤ b) (hsub : Finset.Icc a b ⊆ B) : ¬IsFullyPairedOn κ (Finset.Icc a b)

Primitive and not full means: no nonempty subinterval of the block is fully paired.

theorem Anderson4D.r324Step3_fullyPaired_straddles {n p : ℕ} {κ : PartialPairing (Fin n)} (hL : R324SidePrimitiveNotFull κ (r324SplitBlockLeft n p)) (hR : R324SidePrimitiveNotFull κ (r324SplitBlockRight n p)) {a b : Fin n} (hab : a ≤ b) (hfp : IsFullyPairedOn κ (Finset.Icc a b)) : ↑a < p ∧ p ≤ ↑b

Step 3(b), first half. Every fully paired subinterval of κ₀ contains the split pair {p, p+1}: it starts in the left block and ends in the right block.

theorem Anderson4D.r324Step3_strict_nested {n p : ℕ} {κ : PartialPairing (Fin n)} (hL : R324SidePrimitiveNotFull κ (r324SplitBlockLeft n p)) (hR : R324SidePrimitiveNotFull κ (r324SplitBlockRight n p)) {a₁ b₁ a₂ b₂ : Fin n} (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) (hf₁ : IsFullyPairedOn κ (Finset.Icc a₁ b₁)) (hf₂ : IsFullyPairedOn κ (Finset.Icc a₂ b₂)) : a₁ < a₂ ∧ b₂ < b₁ ∨ a₁ = a₂ ∧ b₁ = b₂ ∨ a₂ < a₁ ∧ b₁ < b₂

Step 3(b), the paper's display. Two fully paired subintervals of κ₀ are either equal or strictly nested. Together with r324Step3_fullyPaired_straddles (each of them straddles the split point) this is exactly

1 ≤ a_t < ⋯ < a₁ ≤ p < p+1 ≤ b₁ < ⋯ < b_t ≤ p+q,

the nested chain that Step 3 reduces one interval at a time. It replaces every form of grading or per-contraction budget: there is a linear order on the surviving intervals.

Step 3(a): the four external legs integrate to constants

theorem Anderson4D.r324Step3_external_legs (x₁ xp xq xr : T4) : (((∫ (x : T4), invSqKer (x - x₁) ∂paperMeasure) * ∫ (y : T4), invSqKer (xp - y) ∂paperMeasure) * ∫ (z : T4), invSqKer (z - xq) ∂paperMeasure) * ∫ (w : T4), invSqKer (xr - w) ∂paperMeasure = invSqKerMass ^ 4

Step 3(a). "In (4.19) we first integrate in (x, y, z, w) yielding constants, leading to (4.20)." Each of the four external legs |x - x₁|⁻², |x_p - y|⁻², |z - x_{p+1}|⁻², |x_{p+q} - w|⁻² integrates to the same finite constant ∫|z|⁻²; the passage from (4.19) to (4.20) costs exactly its fourth power.

Step 3(c): the elementary eight-dimensional integral

"It is then elementary to show that

∫_{T⁸} |x_{a₁-1} - x_{a₁}|⁻² · [(4.4) bound](z) · |x_{b₁} - x_{b₁+1}|⁻² dx_{a₁} dx_{b₁} ≤ C, z := x_{a₁} - x_{b₁},

so we can bound (4.20) by ... ", i.e. the innermost interval [a₁, b₁] of the nested chain is removed at the price of a single constant, and the structure of (4.20) is reassembled with κ₀′ := κ₀ \ κ₁.

noncomputable def Anderson4D.r324Step3EightDimIntegrand (C lam ε supportConstant : ℝ) (k : ℕ) (u v a b : T4) : ℝ

The integrand of the paper's elementary eight-dimensional integral: the chain leg entering a₁, the (4.4) majorant J̃_{k,prim}(x_{a₁} - x_{b₁}) of the primitive pairing induced on [a₁, b₁], and the chain leg leaving b₁.

Equations

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

theorem Anderson4D.exists_r324Step3_elementaryEightDim_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (k : ℕ) (u v : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∫ (a : T4), ∫ (b : T4), r324Step3EightDimIntegrand C lam ε supportConstant k u v a b ∂paperMeasure ∂paperMeasure ≤ (C * lam) ^ (2 * k) * K

Step 3(c), the elementary eight-dimensional integral. Uniformly in the two flanking chain variables u = x_{a₁-1}, v = x_{b₁+1}, in the scale ε and in the length k = k₁ of the removed interval,

∫∫ |u - a|⁻² · J̃_{k,prim}(a - b) · |b - v|⁻² da db ≤ (Cλ)^{2k} · K.

Stripping the (Cλ)^{2k} that (4.4) puts in front of J̃_{k,prim}, the integral is bounded by the single constant K — the paper's "≤ C".

Step 3(d): the induction over the nested chain

theorem Anderson4D.r324Step3_chain_induction {t : ℕ} {Cl K : ℝ} (hCl : 0 ≤ Cl) (hK : 0 ≤ K) (E : ℕ → ℝ) (k : ℕ → ℕ) (hstep : ∀ i < t, E i ≤ Cl ^ (2 * k i) * K * E (i + 1)) : E 0 ≤ Cl ^ (2 * ∑ i ∈ Finset.range t, k i) * K ^ t * E t

Step 3(d). "Now we perform successive reductions for these subintervals ... Iterate over [a₂, b₂], ...". Because the surviving fully paired subintervals form a strictly nested chain (r324Step3_strict_nested), the reductions can be performed one at a time, each gaining (Cλ)^{2 k_i} from (4.4) and costing the single constant K of the elementary eight-dimensional integral. After t steps:

Step 3, last line: (Cλ)^{2m}|log ε|⁻¹ ≤ λ_ε² · C (Cλ)^{2m-2}

theorem Anderson4D.r324Step23_lamEps_sq (lam ε : ℝ) : lamEps lam ε ^ 2 = lam ^ 2 / |Real.log ε|

theorem Anderson4D.r324Step23_output_identity (C lam ε : ℝ) {m : ℕ} (hm : 1 ≤ m) : (C * lam) ^ (2 * m) / |Real.log ε| = lamEps lam ε ^ 2 * C ^ 2 * (C * lam) ^ (2 * m - 2)

The paper's last line of Step 3, verbatim: (Cλ)^{2m}|log ε|⁻¹ ≤ λ_ε² · C (Cλ)^{2m-2}, here as an identity with C = C². This is (3.24) with 1 on the right-hand side, written in the shape the proved consumers use.

Steps 2–3, assembled

The single input the two steps take from the §4.1 iteration is recorded as one named hypothesis, exactly as R324Step1Reduction records it for Step 1.

def Anderson4D.R324Step23Reduction (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (Cred supportConstant : ℝ) : Prop

The one input Steps 2–3 take from the §4.1 iteration.

Everything the paper does between (4.16) and the last line of Step 3 is:

• 2(a) replace the sum over (κ₊, κ₋, π) by a sum over full pairings κ′ of [1, 2m] — proved, and restated here as r324Step2_wick_regroup;
• 2(b), 2(c) identify the fully paired subintervals of κ′ inside [1, m] and inside [m+1, 2m] and fix their positions — the purely positional count card_intervalConfigs_two_mul_le, whose cost is 16^m;
• 2(d), 2(e) write (4.18) and successively sum over the primitive pairings κ_i (i ≥ 1), removing each I_i, gaining a factor Cλ per removal and introducing new inputs H with |H(z)| ≲ |z|⁻² (the §4.1 iteration, verbatim);
• 2(f) only then take absolute values, giving (4.19);
• 3(a) integrate the four external legs, giving (4.20) — r324Step3_external_legs;
• 3(b) the surviving intervals form a strictly nested chain — r324Step3_fullyPaired_straddles, r324Step3_strict_nested;
• 3(c), 3(d) reduce the chain one interval at a time by the elementary eight-dimensional integral — exists_r324Step3_elementaryEightDim_le, r324Step3_chain_induction.

What survives is the last application of (4.4): one primitive block of size k, whose inserted majorant J̃_{k,prim} is integrated once. This hypothesis says exactly that, with the positional cost 16^m and the (Cλ) gained by each removal displayed.

Equations

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

theorem Anderson4D.exists_r324Step23_bound (ρ : SmoothCutoff) {Cred supportConstant : ℝ} (hCred : 0 < Cred) (hsupport : 0 < supportConstant) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ m → R324Step23Reduction ρ lam ε m α β Cred supportConstant → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerC * (powerC * lam) ^ (2 * m - 2)

Steps 2 and 3 of §4.2, complete.

Given the §4.1 successive removal and the nested-chain reduction (the one named hypothesis R324Step23Reduction), the second moment obeys

|E|P̂_m(α,β)|²| ≤ (Cλ)^{2m}|log ε|⁻¹ = λ_ε² · C (Cλ)^{2m-2},

which is (3.24) with 1 on the right-hand side, in the form consumed by the deterministic closure.