The torus model, symmetry class, and cutoff (paper §1.1, Def. 2.1)

Paper: I-torus — the torus model and the normalization ledger

Stable torus and cutoff definitions fixed by the normalization design; see docs/DESIGN.md §5.1 and the blueprint's Conventions section. Blueprint nodes: D-E, parts of I-torus.

Normalization ledger (fixed here once):

• the torus is T4 := Fin 4 → AddCircle (2π); the paper's reference measure is paperMeasure = (2π)⁴ • the product of probability Haar measures (mass (2π)⁴ — Lebesgue on [-π,π]⁴);
• characters are charT4 k x = ∏ i, e^{i k i · x i};
• the ℝ⁴ Fourier transform used for the mollifier multiplier is fourierR4 f ξ = ∫ x, e^{-i⟨x,ξ⟩} f x; this convention makes periodization match the multiplier fourierR4 ρ (ε • k) by Poisson summation;
• the cutoff ρ lives on ℝ⁴ with an explicit support radius; no radius-one rescaling is assumed at fixed ε.

@[reducible, inline]

abbrev Anderson4D.dim : ℕ

Spatial dimension.

Equations

• Anderson4D.dim = 4

@[reducible, inline]

abbrev Anderson4D.Z4 : Type

The frequency lattice ℤ⁴.

Equations

• Anderson4D.Z4 = (Fin Anderson4D.dim → ℤ)

@[reducible, inline]

abbrev Anderson4D.R4 : Type

Euclidean-side space ℝ⁴ (with the sup Pi norm; all constants are norm-choice-dependent and named, DESIGN §5.4).

Equations

• Anderson4D.R4 = (Fin Anderson4D.dim → ℝ)

@[reducible, inline]

abbrev Anderson4D.T4 : Type

The spatial torus 𝕋⁴ = (ℝ/2πℤ)⁴.

Equations

• Anderson4D.T4 = (Fin Anderson4D.dim → AddCircle (2 * Real.pi))

instance Anderson4D.instFactLtRealOfNatHMulPi_anderson4D : Fact (0 < 2 * Real.pi)

noncomputable def Anderson4D.charT4 (k : Z4) (x : T4) : ℂ

Product character e_k(x) = ∏ i, e^{i k_i x_i} (paper's e^{ik·x}).

Equations

• Anderson4D.charT4 k x = ∏ i : Fin Anderson4D.dim, (fourier (k i)) (x i)

@[simp]

theorem Anderson4D.charT4_zero (x : T4) : charT4 0 x = 1

noncomputable def Anderson4D.haarT4 : MeasureTheory.Measure T4

The product of probability Haar measures on T4 (mathlib-normalized side of the measure dictionary).

Equations

• Anderson4D.haarT4 = MeasureTheory.Measure.pi fun (x : Fin Anderson4D.dim) => AddCircle.haarAddCircle

instance Anderson4D.instIsProbabilityMeasureT4HaarT4 : MeasureTheory.IsProbabilityMeasure haarT4

noncomputable def Anderson4D.paperMeasure : MeasureTheory.Measure T4

The paper's reference measure on 𝕋⁴: total mass (2π)⁴ (Lebesgue on [-π,π]⁴).

Equations

• Anderson4D.paperMeasure = ENNReal.ofReal ((2 * Real.pi) ^ Anderson4D.dim) • Anderson4D.haarT4

noncomputable def Anderson4D.fourierR4 (f : R4 → ℝ) (ξ : R4) : ℂ

The ℝ⁴ Fourier transform convention used for mollifier multipliers: (fourierR4 f) ξ = ∫ x, e^{-i⟨x,ξ⟩} f x dx with the plain bilinear pairing ⟨x,ξ⟩ = ∑ i, x i * ξ i and Lebesgue measure.

Equations

• Anderson4D.fourierR4 f ξ = ∫ (x : Anderson4D.R4), Complex.exp (-Complex.I * ↑(∑ i : Fin Anderson4D.dim, x i * ξ i)) * ↑(f x)

structure Anderson4D.MemEClassR4 (f : R4 → ℝ) : Prop

The hyperoctahedral symmetry class 𝓔 for functions on ℝ⁴ (paper Def. 2.1, single-slot B₄ reading): invariance under coordinate permutations and per-coordinate sign flips.

• perm_invariant (σ : Equiv.Perm (Fin dim)) (x : R4) : f (x ∘ ⇑σ) = f x
• even_coord (i : Fin dim) (x : R4) : f (Function.update x i (-x i)) = f x

structure Anderson4D.MemEClassT4 (f : T4 → ℝ) : Prop

The symmetry class 𝓔 on the torus (same B₄ action, descended).

• perm_invariant (σ : Equiv.Perm (Fin dim)) (x : T4) : f (x ∘ ⇑σ) = f x
• even_coord (i : Fin dim) (x : T4) : f (Function.update x i (-x i)) = f x

noncomputable def Anderson4D.flipT4Coords (s : Finset (Fin dim)) (x : T4) : T4

Negate exactly the torus coordinates belonging to s.

Equations

• Anderson4D.flipT4Coords s x i = if i ∈ s then -x i else x i

theorem Anderson4D.flipT4Coords_insert (s : Finset (Fin dim)) (i : Fin dim) (hi : i ∉ s) (x : T4) : flipT4Coords (insert i s) x = Function.update (flipT4Coords s x) i (-flipT4Coords s x i)

theorem Anderson4D.MemEClassT4.flipT4Coords_invariant {f : T4 → ℝ} (hf : MemEClassT4 f) (s : Finset (Fin dim)) (x : T4) : f (flipT4Coords s x) = f x

Membership in 𝓔 gives invariance under any simultaneous collection of coordinate sign flips.

theorem Anderson4D.MemEClassT4.neg_invariant {f : T4 → ℝ} (hf : MemEClassT4 f) (x : T4) : f (-x) = f x

Slotwise evenness implies invariance under simultaneous negation of all four coordinates.

structure Anderson4D.SmoothCutoff : Type

The mollifier class of the paper's §1.1 (blueprint Conventions item 3): smooth, nonnegative, compactly supported with an explicit support radius, in the class 𝓔, integral one. Smoothness is recorded per finite order (robust against smoothness-exponent API differences).

• toFun : R4 → ℝ
• radius : ℝ
• radius_pos : 0 < self.radius
• smooth (n : ℕ) : ContDiff ℝ (↑n) self.toFun
• nonneg (x : R4) : 0 ≤ self.toFun x
• support_subset : Function.support self.toFun ⊆ Metric.ball 0 self.radius
• memE : MemEClassR4 self.toFun
• integral_one : ∫ (x : R4), self.toFun x = 1

@[implicit_reducible]

instance Anderson4D.instCoeFunSmoothCutoffForallR4Real : CoeFun SmoothCutoff fun (x : SmoothCutoff) => R4 → ℝ

Equations

• Anderson4D.instCoeFunSmoothCutoffForallR4Real = { coe := Anderson4D.SmoothCutoff.toFun }

noncomputable def Anderson4D.SmoothCutoff.rescale (ρ : SmoothCutoff) (ε : ℝ) (x : R4) : ℝ

Parabolic rescaling ρ_ε = ε⁻⁴ ρ(·/ε) on ℝ⁴ (paper §1.1).

Equations

• ρ.rescale ε x = ε⁻¹ ^ Anderson4D.dim * ρ.toFun (ε⁻¹ • x)

noncomputable def Anderson4D.SmoothCutoff.eta (ρ : SmoothCutoff) (x : R4) : ℝ

The paper's η = ρ * ρ (convolution on ℝ⁴), entering the noise covariance E[ξ_ε(x)ξ_ε(y)] = η_ε(x-y) (paper (2.3)).

Equations

• ρ.eta x = ∫ (y : Anderson4D.R4), ρ.toFun y * ρ.toFun (x - y)

noncomputable def Anderson4D.SmoothCutoff.symbol (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ℂ

The Fourier multiplier symbol of the mollifier at scale ε: ρ̂(εk), matching periodized convolution by Poisson summation.

Equations

• ρ.symbol ε k = Anderson4D.fourierR4 ρ.toFun fun (i : Fin Anderson4D.dim) => ε * ↑(k i)

noncomputable def Anderson4D.lamEps (lam ε : ℝ) : ℝ

The coupling constant λ_ε = λ / √|log ε| (paper (1.1)); junk for ε ∉ (0,1) per DESIGN §5.7 (the theorem hypotheses exclude it).

Equations

• Anderson4D.lamEps lam ε = lam / √|Real.log ε|

noncomputable def Anderson4D.truncOrder (ε : ℝ) : ℕ

The truncation order A = ⌊|log ε|⌋ (paper (3.11)).

Equations

• Anderson4D.truncOrder ε = ⌊|Real.log ε|⌋₊