The Taylor-cancellation input for R-322

This file connects the local Green Taylor theorem to the actual torus difference in paper (4.9). A compatible-lift hypothesis records the geometric fact that the short displacement does not wrap in the chosen chart. Under the chart-safety and radius hypotheses proved by the local region decomposition, the defined remainder is bounded by C |u|² r⁻⁴. The linear part is a genuine continuous linear functional, so ReductionSymmetry.taylor_cancellation_bound can remove it for every kernel in the paper's class E.

noncomputable def Anderson4D.greenGradientCLM (x : R4) : R4 →L[ℝ] ℝ

The gradient at a local lift, bundled as a continuous linear functional on ℝ⁴.

Equations

• Anderson4D.greenGradientCLM x = ∑ i : Fin Anderson4D.dim, Anderson4D.greenLocalGrad x i • ContinuousLinearMap.proj i

@[simp]

theorem Anderson4D.greenGradientCLM_apply (x h : R4) : (greenGradientCLM x) h = ∑ i : Fin dim, greenLocalGrad x i * h i

theorem Anderson4D.coordinateL1Dist_sq_le_four_euclideanDistSq (a b : R4) : coordinateL1Dist a b ^ 2 ≤ 4 * euclideanDistSq (b - a)

Cauchy--Schwarz in the fixed four-dimensional coordinate chart.

Concatenating Taylor estimates across a periodic seam

theorem Anderson4D.greenLocalLift_coord_taylor_upper_wrap {x : R4} (j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hxj : x j < Real.pi) (hwrap : Real.pi < x j + h) (hhpi : h ≤ Real.pi) (hr : 0 < r) (hradius₁ : ∀ t ∈ Set.Icc 0 (Real.pi - x j), r ≤ √(euclideanDistSq (coordLine x j t))) (hradius₂ : ∀ t ∈ Set.Icc (Real.pi - x j) h, r ≤ √(euclideanDistSq (coordLine (coordLine x j (-2 * Real.pi)) j t))) : |greenLocalLift (coordLine x j h) - greenLocalLift x - greenLocalGrad x j * h| ≤ greenLocalHessSingularBound * r⁻¹ ^ 4 * h ^ 2

One-coordinate Taylor estimate when a positive displacement crosses the upper face of the principal cell.

theorem Anderson4D.greenLocalLift_coord_taylor_lower_wrap {x : R4} (j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hxj : -Real.pi < x j) (hwrap : x j + h < -Real.pi) (hhpi : -Real.pi ≤ h) (hr : 0 < r) (hradius₁ : ∀ t ∈ Set.Icc (-Real.pi - x j) 0, r ≤ √(euclideanDistSq (coordLine x j t))) (hradius₂ : ∀ t ∈ Set.Icc h (-Real.pi - x j), r ≤ √(euclideanDistSq (coordLine (coordLine x j (2 * Real.pi)) j t))) : |greenLocalLift (coordLine x j h) - greenLocalLift x - greenLocalGrad x j * h| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * h ^ 2

One-coordinate Taylor estimate when a negative displacement crosses the lower face of the principal cell.

theorem Anderson4D.greenLocalLift_coord_taylor_no_wrap {x : R4} (j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hlower : -Real.pi ≤ x j + h) (hupper : x j + h ≤ Real.pi) (hr : 0 < r) (hradius : ∀ t ∈ Set.uIcc 0 h, r ≤ √(torusDistSq (greenLocalPoint (coordLine x j t)))) : |greenLocalLift (coordLine x j h) - greenLocalLift x - greenLocalGrad x j * h| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * h ^ 2

One-coordinate Taylor estimate when the whole displacement remains in the chosen closed principal cell.

theorem Anderson4D.greenLocalLift_coord_taylor_from_lower_boundary {x : R4} (j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hxj : x j = -Real.pi) (hneg : h < 0) (hhpi : -Real.pi ≤ h) (hr : 0 < r) (hradius : ∀ t ∈ Set.uIcc 0 h, r ≤ √(torusDistSq (greenLocalPoint (coordLine x j t)))) : |greenLocalLift (coordLine x j h) - greenLocalLift x - greenLocalGrad x j * h| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * h ^ 2

The lower-wrap estimate when the canonical starting coordinate is exactly the half-open-cell boundary -π.

theorem Anderson4D.greenLocalLift_coord_taylor_wrapped {x : R4} (j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hxIco : x j ∈ Set.Ico (-Real.pi) Real.pi) (hh : h ∈ Set.Icc (-Real.pi) Real.pi) (hr : 0 < r) (hradius : ∀ t ∈ Set.uIcc 0 h, r ≤ √(torusDistSq (greenLocalPoint (coordLine x j t)))) : |greenLocalLift (coordLine x j h) - greenLocalLift x - greenLocalGrad x j * h| ≤ 2 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * h ^ 2

Global one-coordinate Taylor estimate on the torus. The displacement is represented in [-π,π]; the proof covers no wrap, upper wrap, lower wrap, and the half-open-boundary starting point.

noncomputable def Anderson4D.wrappedCoordEndpoint (x : R4) (j : Fin dim) (h : ℝ) : R4

Canonical endpoint of a real coordinate displacement.

Equations

• Anderson4D.wrappedCoordEndpoint x j h = Anderson4D.torusLift (Anderson4D.greenLocalPoint (Anderson4D.coordLine x j h))

theorem Anderson4D.wrappedCoordEndpoint_mem_Ico (x : R4) (j : Fin dim) (h : ℝ) (i : Fin dim) : wrappedCoordEndpoint x j h i ∈ Set.Ico (-Real.pi) Real.pi

theorem Anderson4D.wrappedCoordEndpoint_closed (x : R4) (j : Fin dim) (h : ℝ) : InClosedPrincipalCube (wrappedCoordEndpoint x j h)

theorem Anderson4D.greenLocalGrad_coord_lipschitz_wrapped {x : R4} (i j : Fin dim) {h r : ℝ} (hx : InClosedPrincipalCube x) (hxIco : ∀ (k : Fin dim), x k ∈ Set.Ico (-Real.pi) Real.pi) (hh : h ∈ Set.Icc (-Real.pi) Real.pi) (hr : 0 < r) (hradius : ∀ t ∈ Set.uIcc 0 h, r ≤ √(torusDistSq (greenLocalPoint (coordLine x j t)))) : |greenLocalGrad (wrappedCoordEndpoint x j h) i - greenLocalGrad x i| ≤ 4 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * |h|

Wrapped gradient Lipschitz estimate. Each wrap is split at the fundamental-cell seam and the two closed-cell estimates are concatenated.

noncomputable def Anderson4D.r322GreenRemainder (q u : T4) : ℝ

The exact nonlinear remainder in the Green difference from (4.9).

Equations

• Anderson4D.r322GreenRemainder q u = Anderson4D.greenFn q - Anderson4D.greenFn (q - u) - Anderson4D.torusLinearTerm (Anderson4D.greenGradientCLM (Anderson4D.torusLift q)) u

theorem Anderson4D.r322GreenDifference_expansion (q u : T4) : greenFn q - greenFn (q - u) = torusLinearTerm (greenGradientCLM (torusLift q)) u + r322GreenRemainder q u

Wrapped four-coordinate rectangular path

noncomputable def Anderson4D.torusCoordinateCorner (q u : T4) (k : Fin (dim + 1)) : T4

The torus corner obtained after subtracting the first k coordinates of u from q. Unlike coordinateCorner, every intermediate point is intrinsically defined on the torus and hence remains valid across a face of the principal cell.

Equations

• Anderson4D.torusCoordinateCorner q u k i = if ↑i < ↑k then q i - u i else q i

@[simp]

theorem Anderson4D.torusCoordinateCorner_zero (q u : T4) : torusCoordinateCorner q u 0 = q

@[simp]

theorem Anderson4D.torusCoordinateCorner_last (q u : T4) : torusCoordinateCorner q u ⟨dim, ⋯⟩ = q - u

theorem Anderson4D.torusCoordinateCorner_succ (q u : T4) (i : Fin dim) : torusCoordinateCorner q u i.succ = greenLocalPoint (coordLine (torusLift (torusCoordinateCorner q u i.castSucc)) i (-torusLift u i))

Consecutive torus corners are joined by the canonical real lift of the corresponding coordinate of -u.

theorem Anderson4D.torusLift_torusCoordinateCorner_succ (q u : T4) (i : Fin dim) : torusLift (torusCoordinateCorner q u i.succ) = wrappedCoordEndpoint (torusLift (torusCoordinateCorner q u i.castSucc)) i (-torusLift u i)

Canonical real lifts of consecutive torus corners are exactly the wrapped coordinate endpoints used by the one-dimensional estimates.

theorem Anderson4D.abs_le_abs_of_mem_uIcc_zero {a t : ℝ} (ht : t ∈ Set.uIcc 0 a) : |t| ≤ |a|

A point in the unoriented interval from zero to a has absolute value at most |a|.

theorem Anderson4D.norm_greenLocalPoint_coordLine_torusCorner_sub_le (q u : T4) (j : Fin dim) {t : ℝ} (ht : t ∈ Set.uIcc 0 (-torusLift u j)) : ‖greenLocalPoint (coordLine (torusLift (torusCoordinateCorner q u j.castSucc)) j t) - q‖ ≤ ‖u‖

Every intermediate point on a wrapped coordinate edge lies within the torus sup-distance ‖u‖ of the initial point q.

theorem Anderson4D.torusCoordinateCorner_telescope (f : T4 → ℝ) (q u : T4) : f (q - u) - f q = ∑ i : Fin dim, (f (torusCoordinateCorner q u i.succ) - f (torusCoordinateCorner q u i.castSucc))

Exact telescoping along the intrinsic torus rectangular path.

theorem Anderson4D.torusCoordinateCorner_prefix_telescope (f : T4 → ℝ) (q u : T4) (k : Fin (dim + 1)) : f (torusCoordinateCorner q u k) - f q = ∑ i : Fin dim with ↑i < ↑k, (f (torusCoordinateCorner q u i.succ) - f (torusCoordinateCorner q u i.castSucc))

Prefix form of the torus rectangular telescope.

noncomputable def Anderson4D.torusCoordinateL1 (u : T4) : ℝ

The ℓ¹ length of the canonical torus displacement.

Equations

• Anderson4D.torusCoordinateL1 u = ∑ i : Fin Anderson4D.dim, |Anderson4D.torusLift u i|

theorem Anderson4D.torusCoordinateL1_nonneg (u : T4) : 0 ≤ torusCoordinateL1 u

theorem Anderson4D.sum_sq_torusLift_le_torusCoordinateL1_sq (u : T4) : ∑ i : Fin dim, |torusLift u i| ^ 2 ≤ torusCoordinateL1 u ^ 2

theorem Anderson4D.torusCoordinateL1_sq_le_four_torusDistSq (u : T4) : torusCoordinateL1 u ^ 2 ≤ 4 * torusDistSq u

Fixed-dimensional Cauchy--Schwarz for the canonical torus lift.

theorem Anderson4D.torusCoordinateTaylor_decomposition (f : T4 → ℝ) (df : T4 → Fin dim → ℝ) (q u : T4) : f (q - u) - f q - ∑ i : Fin dim, df q i * -torusLift u i = ∑ i : Fin dim, (f (torusCoordinateCorner q u i.succ) - f (torusCoordinateCorner q u i.castSucc) - df (torusCoordinateCorner q u i.castSucc) i * -torusLift u i) + ∑ i : Fin dim, (df (torusCoordinateCorner q u i.castSucc) i - df q i) * -torusLift u i

Exact Taylor decomposition along the wrapped torus rectangular path.

theorem Anderson4D.torusCoordinateTaylor_bound (f : T4 → ℝ) (df : T4 → Fin dim → ℝ) (q u : T4) {M : ℝ} (hM : 0 ≤ M) (hremainder : ∀ (i : Fin dim), |f (torusCoordinateCorner q u i.succ) - f (torusCoordinateCorner q u i.castSucc) - df (torusCoordinateCorner q u i.castSucc) i * -torusLift u i| ≤ 2 * M * |torusLift u i| ^ 2) (hgradient : ∀ (i : Fin dim), |df (torusCoordinateCorner q u i.castSucc) i - df q i| ≤ 4 * M * torusCoordinateL1 u) : |f (q - u) - f q - ∑ i : Fin dim, df q i * -torusLift u i| ≤ 6 * M * torusCoordinateL1 u ^ 2

Abstract quantitative Taylor estimate on the wrapped rectangular path. The coefficient 6 records 2 for the four edge remainders and 4 for moving each intermediate gradient back to the initial point.

theorem Anderson4D.greenLocalGrad_torusCoordinateCorner_le (q u : T4) (i : Fin dim) {r : ℝ} (hr : 0 < r) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (-torusLift u j), r ≤ √(torusDistSq (greenLocalPoint (coordLine (torusLift (torusCoordinateCorner q u j.castSucc)) j t)))) : |greenLocalGrad (torusLift (torusCoordinateCorner q u i.castSucc)) i - greenLocalGrad (torusLift q) i| ≤ 4 * (greenLocalHessSingularBound * r⁻¹ ^ 4) * torusCoordinateL1 u

Moving the Green gradient from any wrapped rectangular-path corner back to the starting point costs at most four times the Hessian bound times the total coordinate length.

theorem Anderson4D.abs_r322GreenRemainder_le_of_wrapped_radius (q u : T4) {r : ℝ} (hr : 0 < r) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (-torusLift u j), r ≤ √(torusDistSq (greenLocalPoint (coordLine (torusLift (torusCoordinateCorner q u j.castSucc)) j t)))) : |r322GreenRemainder q u| ≤ 24 * greenLocalHessSingularBound * r⁻¹ ^ 4 * torusDistSq u

Global torus Taylor estimate for the Green kernel. No chart compatibility hypothesis remains: each coordinate edge is allowed to wrap once and is glued through periodic boundary values and gradients.

theorem Anderson4D.wrapped_path_radius_of_reductionRegion_one (q u : T4) (hregion : 2 * ‖u‖ ≤ ‖q‖) (hq : q ≠ 0) (j : Fin dim) (t : ℝ) (ht : t ∈ Set.uIcc 0 (-torusLift u j)) : √(torusDistSq q) / 4 ≤ √(torusDistSq (greenLocalPoint (coordLine (torusLift (torusCoordinateCorner q u j.castSucc)) j t)))

In region (4.10), every point of every wrapped rectangular edge stays at least √(torusDistSq q) / 4 away from the Green singularity.

theorem Anderson4D.abs_r322GreenRemainder_le_of_reductionRegion_one (q u : T4) (hregion : 2 * ‖u‖ ≤ ‖q‖) (hq : q ≠ 0) : |r322GreenRemainder q u| ≤ 6144 * greenLocalHessSingularBound * invSqKer q ^ 2 * torusDistSq u

Pointwise form of the region-(4.10) Taylor estimate, expressed in the same inverse-square kernel used by Proposition 4.1.

theorem Anderson4D.norm_comp_perm_eq (σ : Equiv.Perm (Fin dim)) (u : T4) : ‖u ∘ ⇑σ‖ = ‖u‖

Coordinate permutations preserve the sup norm on T4.

theorem Anderson4D.norm_update_neg_eq (i : Fin dim) (u : T4) : ‖Function.update u i (-u i)‖ = ‖u‖

A single-coordinate sign flip preserves the sup norm on T4.

noncomputable def Anderson4D.reductionRegionOneKernel (q : T4) (J : T4 → ℝ) (u : T4) : ℝ

Restriction of a kernel to region (4.10), for a fixed outer displacement q.

Equations

• Anderson4D.reductionRegionOneKernel q J u = if 2 * ‖u‖ ≤ ‖q‖ then J u else 0

theorem Anderson4D.reductionRegionOneKernel_memE {J : T4 → ℝ} (hJ : MemEClassT4 J) (q : T4) : MemEClassT4 (reductionRegionOneKernel q J)

Region (4.10) is hyperoctahedrally invariant in its integration variable, so restricting a class-E kernel preserves class E.

theorem Anderson4D.coordinateLinearTerm_green_eq_neg_torusLinearTerm (q u : T4) (hcompat : torusLift (q - u) = torusLift q - torusLift u) : coordinateLinearTerm greenLocalGrad (torusLift q) (torusLift (q - u)) = -torusLinearTerm (greenGradientCLM (torusLift q)) u

If the canonical endpoint lifts differ by the canonical increment lift, the coordinate Taylor linear term is the expected directional derivative.

theorem Anderson4D.taylor_cancellation_bound_weighted {J δ remainder : T4 → ℝ} (hJ : MemEClassT4 J) (D : R4 →L[ℝ] ℝ) {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) (hweighted : ∀ (u : T4), |J u * remainder u| ≤ |J 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

Weighted version of Taylor cancellation. Unlike the generic theorem in ReductionSymmetry, the remainder estimate is required only after multiplication by J. Consequently, geometric Taylor hypotheses need only hold on the support of the region-restricted kernel.

theorem Anderson4D.r322GreenDifference_regionOne_integral_le {J : T4 → ℝ} (hJ : MemEClassT4 J) (q : T4) (hq : q ≠ 0) (hmoment : ∀ (i : Fin dim), MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * torusLift u i) paperMeasure) (hintR : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * r322GreenRemainder q u) paperMeasure) (hintMajorant : MeasureTheory.Integrable (fun (u : T4) => |reductionRegionOneKernel q J u| * (6144 * greenLocalHessSingularBound * invSqKer q ^ 2 * torusDistSq u)) paperMeasure) : |∫ (u : T4), reductionRegionOneKernel q J u * (greenFn q - greenFn (q - u)) ∂paperMeasure| ≤ ∫ (u : T4), |reductionRegionOneKernel q J u| * (6144 * greenLocalHessSingularBound * invSqKer q ^ 2 * torusDistSq u) ∂paperMeasure

Integrated region-(4.10) cancellation. The linear Green term is removed by class-E symmetry; only the quadratic remainder survives.

theorem Anderson4D.abs_r322GreenRemainder_le_of_safe_lifts (q u : T4) {r : ℝ} (hr : 0 < r) (hcompat : torusLift (q - u) = torusLift q - torusLift u) (hopen : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift (q - u) j - torusLift q j), InOpenPrincipalCube (coordLine (coordinateCorner (torusLift q) (torusLift (q - u)) j.castSucc) j t)) (hradius : ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift (q - u) j - torusLift q j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner (torusLift q) (torusLift (q - u)) j.castSucc) j t))) : |r322GreenRemainder q u| ≤ 8 * greenLocalHessSingularBound * r⁻¹ ^ 4 * torusDistSq u

The quantitative remainder estimate behind paper (4.9), on a safe local chart. The factor 8 is 2 from the rectangular Taylor theorem times 4 from ℓ¹² ≤ 4ℓ²².

theorem Anderson4D.r322GreenDifference_integral_le_of_safe_lifts {J : T4 → ℝ} (hJ : MemEClassT4 J) (q : T4) {r : ℝ} (hr : 0 < r) (hcompat : ∀ (u : T4), J u ≠ 0 → torusLift (q - u) = torusLift q - torusLift u) (hopen : ∀ (u : T4), J u ≠ 0 → ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift (q - u) j - torusLift q j), InOpenPrincipalCube (coordLine (coordinateCorner (torusLift q) (torusLift (q - u)) j.castSucc) j t)) (hradius : ∀ (u : T4), J u ≠ 0 → ∀ (j : Fin dim), ∀ t ∈ Set.uIcc 0 (torusLift (q - u) j - torusLift q j), r ≤ √(euclideanDistSq (coordLine (coordinateCorner (torusLift q) (torusLift (q - u)) j.castSucc) j t))) (hmoment : ∀ (i : Fin dim), MeasureTheory.Integrable (fun (u : T4) => J u * torusLift u i) paperMeasure) (hintR : MeasureTheory.Integrable (fun (u : T4) => J u * r322GreenRemainder q u) paperMeasure) (hintMajorant : MeasureTheory.Integrable (fun (u : T4) => |J u| * (8 * greenLocalHessSingularBound * r⁻¹ ^ 4 * torusDistSq u)) paperMeasure) : |∫ (u : T4), J u * (greenFn q - greenFn (q - u)) ∂paperMeasure| ≤ ∫ (u : T4), |J u| * (8 * greenLocalHessSingularBound * r⁻¹ ^ 4 * torusDistSq u) ∂paperMeasure

Integrated Taylor cancellation on a safe chart. Every premise other than integrability is discharged from the concrete Green construction and the geometric chart conditions above.