Symmetry and local analytic interfaces for the reduction in paper §4.1

This file isolates the analytic mechanisms used in (4.8)--(4.12).

• coordinateFlipT4 preserves the paper measure.
• If J ∈ 𝓔, every coordinate of its first moment (using the canonical torus lift) vanishes. The boundary ambiguity of the lift at -π is handled as an almost-everywhere statement, not silently ignored.
• quadratic_remainder_of_lipschitz_fderiv supplies a reusable, genuinely differentiable version of the second-order Taylor estimate in (4.9).
• taylor_cancellation_bound removes the linear term and retains only the quadratic majorant.
• The three measurable regions from (4.10)--(4.12) are bounded by the already-proved three-kernel convolution estimate. Product integrability is explicit, so no result relies on Lean's junk value for a non-integrable Bochner integral.

The remaining ε/|log ε| radial bookkeeping for the primitive kernel belongs to the final R-322 assembly, not to these interfaces.

Coordinate flips and odd first moments

noncomputable def Anderson4D.coordinateFlipT4 (i : Fin dim) (x : T4) : T4

Flip one coordinate of the four-dimensional torus.

Equations

• Anderson4D.coordinateFlipT4 i x = Function.update x i (-x i)

noncomputable def Anderson4D.coordinateFlipMeasurableEquiv (i : Fin dim) : T4 ≃ᵐ T4

The coordinate flip, bundled as a measurable involution.

Equations

• Anderson4D.coordinateFlipMeasurableEquiv i = { toEquiv := Function.Involutive.toPerm (Anderson4D.coordinateFlipT4 i) ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem Anderson4D.coordinateFlipMeasurableEquiv_apply (i : Fin dim) (x : T4) : (coordinateFlipMeasurableEquiv i) x = coordinateFlipT4 i x

theorem Anderson4D.measurePreserving_coordinateFlipT4 (i : Fin dim) : MeasureTheory.MeasurePreserving (⇑(coordinateFlipMeasurableEquiv i)) paperMeasure paperMeasure

A single-coordinate sign flip preserves the paper's Lebesgue normalization on 𝕋⁴.

theorem Anderson4D.ae_torusLift_coordinateFlip (i : Fin dim) : ∀ᵐ (x : T4) ∂paperMeasure, torusLift (coordinateFlipT4 i x) i = -torusLift x i

The canonical lift is odd under a coordinate flip away from the measure-zero boundary of the half-open fundamental domain.

theorem Anderson4D.eClass_coordinate_moment_eq_zero {J : T4 → ℝ} (hJ : MemEClassT4 J) (i : Fin dim) (_hint : MeasureTheory.Integrable (fun (u : T4) => J u * torusLift u i) paperMeasure) : ∫ (u : T4), J u * torusLift u i ∂paperMeasure = 0

The i-th first moment of an 𝓔-symmetric kernel vanishes.

The integrability hypothesis is deliberate: without it, the Bochner integral is junk-totalized to zero and the statement would not certify the analytic cancellation used in (4.9).

noncomputable def Anderson4D.torusLinearTerm (D : R4 →L[ℝ] ℝ) (u : T4) : ℝ

The linear form in (4.9), evaluated on the canonical lift.

Equations

• Anderson4D.torusLinearTerm D u = D (Anderson4D.torusLift u)

theorem Anderson4D.eClass_linear_moment_eq_zero {J : T4 → ℝ} (hJ : MemEClassT4 J) (D : R4 →L[ℝ] ℝ) (hint : ∀ (i : Fin dim), MeasureTheory.Integrable (fun (u : T4) => J u * torusLift u i) paperMeasure) : ∫ (u : T4), J u * torusLinearTerm D u ∂paperMeasure = 0

Every linear first moment of an 𝓔-symmetric kernel vanishes.

A genuine second-order Taylor interface

theorem Anderson4D.quadratic_remainder_of_lipschitz_fderiv {f : R4 → ℝ} {df : R4 → R4 →L[ℝ] ℝ} {a b : R4} {M : ℝ} (hM : 0 ≤ M) (hderiv : ∀ x ∈ segment ℝ a b, HasFDerivWithinAt f (df x) (segment ℝ a b) x) (hLip : ∀ x ∈ segment ℝ a b, ‖df x - df a‖ ≤ M * ‖x - a‖) : |f b - f a - (df a) (b - a)| ≤ M * ‖b - a‖ ^ 2

A Lipschitz bound on the Fréchet derivative along a segment gives the quadratic Taylor remainder needed in (4.9).

theorem Anderson4D.taylor_cancellation_bound {J δ remainder : T4 → ℝ} (hJ : MemEClassT4 J) (D : R4 →L[ℝ] ℝ) {C : ℝ} (_hC : 0 ≤ C) (hmoment : ∀ (i : Fin dim), MeasureTheory.Integrable (fun (u : T4) => J u * torusLift u i) paperMeasure) (hexpand : ∀ (u : T4), δ u = -torusLinearTerm D u + remainder u) (hremainder : ∀ (u : T4), |remainder u| ≤ C * torusDistSq u) (hintR : MeasureTheory.Integrable (fun (u : T4) => J u * remainder u) paperMeasure) (hintMajorant : MeasureTheory.Integrable (fun (u : T4) => |J u| * (C * torusDistSq u)) paperMeasure) : |∫ (u : T4), J u * δ u ∂paperMeasure| ≤ ∫ (u : T4), |J u| * (C * torusDistSq u) ∂paperMeasure

Integrated Taylor cancellation: if δ is a linear term plus a quadratic remainder, 𝓔-symmetry removes the linear contribution and the integral is controlled only by the quadratic majorant.

Three local regions from (4.10)--(4.12)

noncomputable def Anderson4D.reductionTripleKernel (x : T4) (p : T4 × T4) : ℝ

The nonnegative three-kernel majorant after translating y to the origin. The pair is (z,w).

Equations

• Anderson4D.reductionTripleKernel x p = Anderson4D.invSqKer (x - p.1) * Anderson4D.invSqKer (p.1 - p.2) * Anderson4D.invSqKer p.2

theorem Anderson4D.reductionTripleKernel_nonneg (x : T4) (p : T4 × T4) : 0 ≤ reductionTripleKernel x p

def Anderson4D.reductionRegion₁ : Set (T4 × T4)

Case (4.10): the increment z-w is small compared with z-y (with y translated to zero).

Equations

• Anderson4D.reductionRegion₁ = {p : Anderson4D.T4 × Anderson4D.T4 | 2 * ‖p.1 - p.2‖ ≤ ‖p.1‖}

def Anderson4D.reductionRegion₂ : Set (T4 × T4)

Case (4.11): z-y is no larger than the increment and z-w is comparable with w-y.

Equations

• Anderson4D.reductionRegion₂ = {p : Anderson4D.T4 × Anderson4D.T4 | ‖p.1‖ ≤ 2 * ‖p.1 - p.2‖ ∧ ‖p.1 - p.2‖ ≤ 2 * ‖p.2‖ ∧ ‖p.2‖ ≤ 2 * ‖p.1 - p.2‖}

def Anderson4D.reductionRegion₃ : Set (T4 × T4)

Case (4.12): w-y is no larger than the increment and z-w is comparable with z-y.

Equations

• Anderson4D.reductionRegion₃ = {p : Anderson4D.T4 × Anderson4D.T4 | ‖p.2‖ ≤ 2 * ‖p.1 - p.2‖ ∧ ‖p.1 - p.2‖ ≤ 2 * ‖p.1‖ ∧ ‖p.1‖ ≤ 2 * ‖p.1 - p.2‖}

theorem Anderson4D.measurableSet_reductionRegion₁ : MeasurableSet reductionRegion₁

theorem Anderson4D.measurableSet_reductionRegion₂ : MeasurableSet reductionRegion₂

theorem Anderson4D.measurableSet_reductionRegion₃ : MeasurableSet reductionRegion₃

theorem Anderson4D.reduction_three_local_integrals_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4), MeasureTheory.Integrable (reductionTripleKernel x) (paperMeasure.prod paperMeasure) → ∫ (p : T4 × T4) in reductionRegion₁, reductionTripleKernel x p ∂paperMeasure.prod paperMeasure ≤ C ∧ ∫ (p : T4 × T4) in reductionRegion₂, reductionTripleKernel x p ∂paperMeasure.prod paperMeasure ≤ C ∧ ∫ (p : T4 × T4) in reductionRegion₃, reductionTripleKernel x p ∂paperMeasure.prod paperMeasure ≤ C

The three local integrals corresponding to (4.10)--(4.12) are uniformly bounded by the same absolute constant as the unrestricted threefold singular convolution.

The joint Integrable premise is exposed because it is precisely what licenses Fubini and prevents a junk-totalized integral. In the R-322 assembly it is discharged by the primitive-kernel radial bounds.