Paper §4.2, Step 1: the deterministic (full-pairing) terms

Paper: R-324 — §4.2 Step 1 — the deterministic terms (κ a full pairing)

This file transcribes Step 1 of Section 4.2 of arXiv:2607.10105v1 (pages 18–19) literally, in the paper's own order.

After the successive removal of the fully paired subintervals (the §4.1 iteration, recorded here as the single named hypothesis R324Step1Reduction), the paper is left with (4.17): a four-fold integral in (x_a, x_m, x, y) carrying (Cλ)^{m-2p} in front,

∫ e^{i(α·x+β·y)} G₀(x-x_a) J_{2p,prim}(x_a-x_m)
    [G(x_m-y) - G(x_a-y)] dx_a dx_m dx dy .

This is r324Step1Integral. The remaining five moves of Step 1 are

1. r324Step1_integral_y — the y-integral produces ⟨β⟩⁻²(e^{iβ·x_m} - e^{iβ·x_a}), i.e. the paper's ⟨β⟩⁻² e^{iβ·x_a}(e^{iβ·(x_m-x_a)} - 1);
2. r324Step1_integral_x — the x-integral of G₀ produces ⟨α⟩⁻² e^{iα·x_a};
3. r324Step1_integral_xm — translating x_m = x_a + u and using J_{2p,prim} ∈ 𝓔 (Proposition 4.1) makes the imaginary part sin(β·(x_m-x_a)) integrate to zero, leaving cos - 1;
4. r324Step1_beta_cosine_le — the surviving real part obeys ⟨β⟩⁻²|cos(β·z)-1| ≤ |z|², which is the (4.4) insertion, so J_{2p,prim} is replaced by J̃_{2p,prim};
5. r324Step1_norm_le / exists_r324Step1_bound — integrating J̃ in x_m, G₀ in x and finally in x_a gives (Cλ)^{2p}|log ε|⁻¹, hence (Cλ)^m|log ε|⁻¹, which is (3.24).

Every analytic input is a proved theorem: proposition41_at_truncation (4.3)–(4.4) and J ∈ 𝓔; integral_charT4_mul_greenFn_shift (Ĝ(β) = ⟨β⟩⁻²); integral_memEClass_mul_characterSubOne_eq_cos (the 𝓔-symmetry cancellation); abs_r324CharacterCos_sub_one_le_half_mul (the sharp cosine bound); torusDistSq_mul_primitiveKernelMajorant_le_max_one_sq_mul_inserted (the J ↦ J̃ replacement at the level of the two majorants); and exists_integral_primitiveInsertedMajorant_le (the final radial integration).

The expression (4.17)

noncomputable def Anderson4D.r324Step1Integrand (J : T4 → ℝ) (α β : Z4) (xa xm x y : T4) : ℂ

The integrand of (4.17): e^{i(α·x+β·y)} G₀(x-x_a) J(x_a-x_m) [G(x_m-y) - G(x_a-y)], with the primitive kernel J kept abstract.

Equations

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

noncomputable def Anderson4D.r324Step1Integral (J : T4 → ℝ) (α β : Z4) : ℂ

The second display of (4.17), integrated in the paper's own order: y innermost, then x, then x_m, then x_a.

Equations

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

Step 1(a): the y-integral

theorem Anderson4D.r324Step1_integral_y (J : T4 → ℝ) (α β : Z4) (xa xm x : T4) : ∫ (y : T4), r324Step1Integrand J α β xa xm x y ∂paperMeasure = charT4 α x * ↑(greenFn (x - xa)) * ↑(J (xa - xm)) * (↑(paperSecondOrderModeDecay β) * (charT4 β xm - charT4 β xa))

The y-integral of (4.17). The paper's

∫ e^{iβ·y}(G(x_m-y) - G(x_a-y)) dy = ⟨β⟩⁻² e^{iβ·x_a}(e^{iβ·(x_m-x_a)} - 1),

recorded in the equivalent un-factored form ⟨β⟩⁻²(e^{iβ·x_m} - e^{iβ·x_a}).

Step 1(b): the x-integral of G₀

theorem Anderson4D.r324Step1_integral_x (J : T4 → ℝ) (α β : Z4) (xa xm : T4) : ∫ (x : T4), ∫ (y : T4), r324Step1Integrand J α β xa xm x y ∂paperMeasure ∂paperMeasure = charT4 α xa * ↑(paperSecondOrderModeDecay α) * (↑(J (xa - xm)) * (↑(paperSecondOrderModeDecay β) * (charT4 β xm - charT4 β xa)))

The x-integral of (4.17). The free boundary leg G₀(x - x_a) against e^{iα·x} is again Ĝ(α) = ⟨α⟩⁻², transported to the base point x_a.

Step 1(c): the x_m-integral and the vanishing imaginary part

theorem Anderson4D.r324Step1_integral_xm {J : T4 → ℝ} (hJ : MemEClassT4 J) (α β : Z4) (xa : T4) (hcos : MeasureTheory.Integrable (fun (u : T4) => J u * (r324CharacterCos β u - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (u : T4) => J u * r324CharacterSin β u) paperMeasure) : ∫ (xm : T4), ∫ (x : T4), ∫ (y : T4), r324Step1Integrand J α β xa xm x y ∂paperMeasure ∂paperMeasure ∂paperMeasure = charT4 α xa * ↑(paperSecondOrderModeDecay α) * (↑(paperSecondOrderModeDecay β) * charT4 β xa) * ∫ (u : T4), ↑(J u * (r324CharacterCos β u - 1)) ∂paperMeasure

The x_m-integral of (4.17). Setting x_m = x_a + u turns the kernel argument into -u; since J_{2p,prim} ∈ 𝓔 (Proposition 4.1) the kernel is even, so the odd component sin(β·u) of the phase integrates to zero and only cos(β·u) - 1 survives. This is the paper's sentence "if we take the imaginary part sin(β·(x_m-x_a)) above, then the contribution to the whole integral vanishes because J_{2p,prim} ∈ E".

Step 1(d): the final x_a-integral

noncomputable def Anderson4D.r324PaperTorusMass : ℝ

Total paperMeasure mass of 𝕋⁴, namely (2π)⁴.

Equations

• Anderson4D.r324PaperTorusMass = (2 * Real.pi) ^ Anderson4D.dim

theorem Anderson4D.r324PaperTorusMass_pos : 0 < r324PaperTorusMass

theorem Anderson4D.r324Step1_norm_le {J : T4 → ℝ} (hJ : MemEClassT4 J) (α β : Z4) (hcos : MeasureTheory.Integrable (fun (u : T4) => J u * (r324CharacterCos β u - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (u : T4) => J u * r324CharacterSin β u) paperMeasure) : ‖r324Step1Integral J α β‖ ≤ r324PaperTorusMass * (paperSecondOrderModeDecay β * ‖∫ (u : T4), ↑(J u * (r324CharacterCos β u - 1)) ∂paperMeasure‖)

The three remaining integrations of Step 1. After J̃ has been integrated in x_m and G₀ in x, the last integration in x_a sees only unimodular characters, so it costs the total mass (2π)⁴. The ⟨α⟩⁻² produced by the x-integral is discarded against 1.

Step 1(e): ⟨β⟩⁻²|cos - 1| is the (4.4) insertion

theorem Anderson4D.r324Step1_modeNormSq_mul_decay_le_one (b : Z4) : paperModeNormSq b * paperSecondOrderModeDecay b ≤ 1

⟨β⟩⁻²|β|² ≤ 1: the bracket produced by the y-integral pays exactly for the two derivatives extracted from cos(β·z) - 1.

theorem Anderson4D.r324Step1_beta_cosine_le (ρ : SmoothCutoff) (lam ε : ℝ) (p : ℕ) (hp : 1 ≤ p) (G : Fin (2 * p - 1) → T4 → ℝ) (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (β : Z4) (hbound : PrimitiveKernelBounds ρ lam ε p hp G supportConstant primitiveConstant) : paperSecondOrderModeDecay β * ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε p hp G u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 1 / 2 * (max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant p z ∂paperMeasure)

The paper's Step 1 inequality ⟨β⟩⁻²|cos(β·(x_m-x_a)) - 1| ≤ ⟨β⟩⁻²|β|²|x_m-x_a|² ≤ ε² + max|x_i-x_j|², in the integrated form the argument actually uses: the surviving real part, weighted by ⟨β⟩⁻², is bounded by the (4.3) majorant carrying one squared-distance insertion — which is exactly (4.4), the J ↦ J̃ replacement.

Step 1(f): the closed estimate for one primitive full pairing

theorem Anderson4D.r324Step1_primitive_norm_le (ρ : SmoothCutoff) (lam ε : ℝ) (p : ℕ) (hp : 1 ≤ p) (G : Fin (2 * p - 1) → T4 → ℝ) (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hC : 0 ≤ primitiveConstant) (hlam : 0 ≤ lam) (α β : Z4) (hJ : MemEClassT4 (primitiveKernelDiff ρ lam ε p hp G)) (hbound : PrimitiveKernelBounds ρ lam ε p hp G supportConstant primitiveConstant) (hcos : MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε p hp G u * (r324CharacterCos β u - 1)) paperMeasure) (hsin : MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε p hp G u * r324CharacterSin β u) paperMeasure) : ‖r324Step1Integral (primitiveKernelDiff ρ lam ε p hp G) α β‖ ≤ r324PaperTorusMass * (1 / 2 * (max 1 (supportConstant ^ 2) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant p z ∂paperMeasure))

Step 1 of §4.2, assembled. The (4.17) integral for a primitive full pairing on 2p elements is bounded by the integrated (4.4) majorant.

Step 1(g): the paper's numerical output (Cλ)^{2p}|log ε|⁻¹

theorem Anderson4D.exists_r324Step1_bound (ρ : SmoothCutoff) : ∃ (Cstep : ℝ), 0 < Cstep ∧ ∀ (lam ε : ℝ) (p : ℕ) (hp : 1 ≤ p) (G : Fin (2 * p - 1) → T4 → ℝ) (α β : Z4), 0 < lam → 0 < ε → ε ≤ 1 → p ≤ truncOrder ε → 1 ≤ |Real.log ε| → IsAdmissiblePrimitiveInput p G → MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε p hp G u * (r324CharacterCos β u - 1)) paperMeasure → MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε p hp G u * r324CharacterSin β u) paperMeasure → ‖r324Step1Integral (primitiveKernelDiff ρ lam ε p hp G) α β‖ ≤ (Cstep * lam) ^ (2 * p) / |Real.log ε|

Step 1 of §4.2, in the paper's own numerical shape.

For every primitive full pairing on 2p elements whose inputs G_j are the admissible functions produced by the successive removal (G_j ∈ 𝓔, |G_j(z)| ≤ |z|⁻²), the (4.17) integral obeys

|(4.17)| ≤ (C λ)^{2p} / |log ε|

with one constant C depending on the mollifier alone. This is the paper's "|P̂_m(α,β)| ≤ (Cλ)^m |log ε|⁻¹" with the (Cλ)^{m-2p} gained by the removal steps still to be multiplied in.

Step 1, first move: the successive removal of §4.1

def Anderson4D.R324Step1Reduction (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (Cred : ℝ) (P : ℂ) : Prop

The one input Step 1 takes from the §4.1 iteration.

P stands for the full-pairing (deterministic) part of (4.16) at order m. The paper takes the maximal-and-rightmost interval I_* = [a, m], removes the fully paired subintervals to the left of I_* and then those inside it one at a time; each removal invokes Proposition 4.1, gains a factor Cλ, and replaces the removed contribution by a new input H with |H(z)| ≲ |z|⁻², which is (4.13). What survives is a primitive full pairing κ_* on 2p elements together with the expression (4.17) — precisely r324Step1Integral applied to J_{2p,prim} = primitiveKernelDiff with the H's as inputs.

This is the closed R-322 chain (exists_r322RenormFiberReductionOutputAE, exists_renormC_bound_of_reduction_ae) transported from §4.1 to the order-m deterministic fibre; the paper says explicitly that §4.2 argues "as in Section 4.1". It is the only move of Step 1 not discharged in this file; everything after it is proved above.

Equations

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

theorem Anderson4D.exists_r324Step1_deterministic_bound (ρ : SmoothCutoff) {Cred : ℝ} (hCred : 0 < Cred) : ∃ (Cdet : ℝ), 0 < Cdet ∧ ∀ (lam ε : ℝ) (m : ℕ) (α β : Z4) (P : ℂ), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324Step1Reduction ρ lam ε m α β Cred P → ‖P‖ ≤ (Cdet * lam) ^ m / |Real.log ε|

Step 1 of §4.2, complete.

Given the §4.1 successive removal, the deterministic (full-pairing) part of (4.16) satisfies

|P̂_m(α,β)| ≤ (Cλ)^m |log ε|⁻¹,

which is (3.24) with 1 on the right-hand side. The (Cλ)^{m-2p} gained by the removals and the (Cλ)^{2p}|log ε|⁻¹ produced by the y-, x- and x_a-integrations recombine into a single power.