High-frequency cutoff payoff for R-324

This file supplies the deterministic multiplier estimate used in paper §4.2, Step 4. Once the routing argument selects a noise frequency of size at least sqrt ε / 2 times the total external frequency, rapid Fourier decay of the cutoff gives the central ⟨ε²(α+β)⟩⁻⁸ payoff.

The result is deliberately below the probability layer: it concerns only the deterministic cutoff symbol and the lattice frequency selected after the Wick expansion.

theorem Anderson4D.SmoothCutoff.euclideanFrequency_scaled_z4 (ε : ℝ) (k : Z4) : (euclideanFrequency fun (i : Fin dim) => ε * ↑(k i)) = (ε / (2 * Real.pi)) • z4EuclideanFrequency k

Exact comparison between the frequency convention of the Euclidean Schwartz transform and the unscaled lattice frequency used by the parametrix.

theorem Anderson4D.SmoothCutoff.norm_euclideanFrequency_scaled_z4 {ε : ℝ} (hε : 0 ≤ ε) (k : Z4) : ‖euclideanFrequency fun (i : Fin dim) => ε * ↑(k i)‖ = ε / (2 * Real.pi) * ‖z4EuclideanFrequency k‖

Norm form of euclideanFrequency_scaled_z4 on positive scales.

theorem Anderson4D.SmoothCutoff.eps_sq_mul_le_sixteen_mul_norm_euclideanFrequency {ε L : ℝ} {k : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hL : 0 ≤ L) (hroute : √ε / 2 * L ≤ ‖z4EuclideanFrequency k‖) : ε ^ 2 * L ≤ 16 * ‖euclideanFrequency fun (i : Fin dim) => ε * ↑(k i)‖

The routed lattice mode is large enough at the actual Schwartz frequency scale. The numerical constant 16 harmlessly absorbs the project's 2π Fourier convention.

theorem Anderson4D.SmoothCutoff.one_add_norm_decay_le_routed_decay {ε L : ℝ} {k : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hL : 0 ≤ L) (hroute : √ε / 2 * L ≤ ‖z4EuclideanFrequency k‖) : ((1 + ‖euclideanFrequency fun (i : Fin dim) => ε * ↑(k i)‖) ^ 8)⁻¹ ≤ 16 ^ 8 * eighthOrderFrequencyDecay (ε ^ 2 * L)

Polynomial decay at Schwartz frequency controls the Japanese bracket used in (3.24), once the routed mode is selected.

theorem Anderson4D.SmoothCutoff.exists_r324_highFrequency_symbol_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε L : ℝ} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → √ε / 2 * L ≤ ‖z4EuclideanFrequency k‖ → ‖ρ.symbol ε k‖ ≤ C * eighthOrderFrequencyDecay (ε ^ 2 * L)

Paper §4.2, Step 4 at the level of a single selected cutoff multiplier. The constant depends only on the fixed cutoff.