Shifted-window lattice sums for the general-m cross peel

The proved complement-schedule closure bounded the diagonal window Σ_k ‖ρ̂(εk)‖⁴⟨k⟩⁻⁴ ≤ C(ρ)|log ε|. The general-m peel meets translated windows Σ_k ‖ρ̂(εk)‖²⟨k+α⟩⁻²⟨k+β⟩⁻². This file proves the shifted bounds, uniformly in the shifts, with per-mollifier constants:

• r324SW_symbol_mass_le — total symbol mass Σ_k ‖ρ̂(εk)‖² ≤ C ε⁻⁴;
• r324SW_translated_window_le_log — Σ_k ‖ρ̂(εk)‖²⟨k+γ⟩⁻⁴ ≤ C|log ε|;
• r324SW_shifted_window_le_log — the bilinear form, via 2xy ≤ x²+y²;
• r324SW_separated_window_le_log — the decay-retaining variant with the ⟨α-β⟩⁻⁴ separation factor.

theorem Anderson4D.r324SW_symbol_sq_le_of_decay_eight (ρ : SmoothCutoff) {C0 : ℝ} (hdecay : ∀ (ξ : R4), (1 + ‖SmoothCutoff.euclideanFrequency ξ‖) ^ 8 * ‖fourierR4 ρ.toFun ξ‖ ≤ C0) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (k : Z4) : ‖ρ.symbol ε k‖ ^ 2 ≤ C0 ^ 2 * (2 * Real.pi) ^ 8 * (ε⁻¹ ^ 8 * ((1 + ↑(z4SupRadius k)) ^ 8)⁻¹)

Degree-four decay of the scaled symbol against the sup bracket, squared: the degree-eight companion of symbol_sq_le_of_decay.

theorem Anderson4D.r324SW_summable_symbol_sq (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 2

The squared scaled symbol is summable over the frequency lattice.

theorem Anderson4D.r324SW_symbol_mass_le (ρ : SmoothCutoff) : ∃ (CM : ℝ), 0 < CM ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 ≤ CM * ε⁻¹ ^ 4

Total symbol mass. The ε-cube carries ≲ ε⁻⁴ unit terms and the degree-8 decay pays the eighth-order radial tail, so Σ_k ‖ρ̂(εk)‖² ≤ C(ρ) ε⁻⁴.

theorem Anderson4D.r324SW_bracket4 (m : Z4) : (1 + paperModeNormSq m)⁻¹ ^ 2 ≤ 4 * ((1 + ↑(z4SupRadius m)) ^ 4)⁻¹

The squared Euclidean bracket dominated by the fourth-order sup bracket, at an arbitrary lattice point.

theorem Anderson4D.r324SW_bracket_le_one (m : Z4) : (1 + paperModeNormSq m)⁻¹ ≤ 1

The Euclidean bracket is at most one.

theorem Anderson4D.r324SW_bracket_nonneg (m : Z4) : 0 ≤ (1 + paperModeNormSq m)⁻¹

theorem Anderson4D.r324SW_summable_translated_window (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (γ : Z4) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 2 * (1 + paperModeNormSq (k + γ))⁻¹ ^ 2

The translated-window integrand is summable, for every shift.

theorem Anderson4D.r324SW_translated_window_le_log (ρ : SmoothCutoff) : ∃ (CT : ℝ), 0 < CT ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (γ : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 * (1 + paperModeNormSq (k + γ))⁻¹ ^ 2 ≤ CT * |Real.log ε|

The translated window is logarithmic, uniformly in the shift. The head is the cube |k+γ|_∞ ≤ ⌈ε⁻¹⌉, which re-centers to the proved diagonal harmonic-shell estimate; outside it the bracket is ≤ 4ε⁴ pointwise and the total symbol mass pays the ε⁻⁴.

theorem Anderson4D.r324SW_summable_shifted_window (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 2 * ((1 + paperModeNormSq (k + α))⁻¹ * (1 + paperModeNormSq (k + β))⁻¹)

The bilinear shifted-window integrand is summable.

theorem Anderson4D.r324SW_shifted_window_le_log (ρ : SmoothCutoff) : ∃ (CS : ℝ), 0 < CS ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (α β : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 * ((1 + paperModeNormSq (k + α))⁻¹ * (1 + paperModeNormSq (k + β))⁻¹) ≤ CS * |Real.log ε|

The shifted window is logarithmic, uniformly in both shifts. 2xy ≤ x² + y² splits the bilinear window into the two translated quartic windows.

theorem Anderson4D.r324SW_translated_window_quartic_le_log (ρ : SmoothCutoff) : ∃ (CT : ℝ), 0 < CT ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (γ : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 4 * (1 + paperModeNormSq (k + γ))⁻¹ ^ 2 ≤ CT * |Real.log ε|

Quartic-symbol variant of the translated window: immediate from ‖ρ̂‖ ≤ 1.

theorem Anderson4D.r324SW_shifted_window_sub_le_log (ρ : SmoothCutoff) : ∃ (CS : ℝ), 0 < CS ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (α β : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 * ((1 + paperModeNormSq (k - α))⁻¹ * (1 + paperModeNormSq (k - β))⁻¹) ≤ CS * |Real.log ε|

Subtracted orientation of the shifted window, for peels that produce k - α normal forms.

theorem Anderson4D.r324SW_shifted_window_quartic_le_log (ρ : SmoothCutoff) : ∃ (CS : ℝ), 0 < CS ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (α β : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 4 * ((1 + paperModeNormSq (k + α))⁻¹ * (1 + paperModeNormSq (k + β))⁻¹) ≤ CS * |Real.log ε|

Quartic-symbol variant of the shifted window: immediate from ‖ρ̂‖ ≤ 1.

theorem Anderson4D.r324SW_bracket_separation (α β k : Z4) : (1 + paperModeNormSq (k + α))⁻¹ ^ 2 * (1 + paperModeNormSq (k + β))⁻¹ ^ 2 ≤ 16 * (1 + paperModeNormSq (α - β))⁻¹ ^ 2 * ((1 + paperModeNormSq (k + α))⁻¹ ^ 2 + (1 + paperModeNormSq (k + β))⁻¹ ^ 2)

Bracket separation. The product of two shifted quartic brackets retains the separation of the shifts: with a = ⟨k+α⟩², b = ⟨k+β⟩², d = ⟨α-β⟩² one has a⁻²b⁻² ≤ 16 d⁻² (a⁻² + b⁻²), because d ≤ 2a + 2b ≤ 4·max.

theorem Anderson4D.r324SW_separated_window_le_log (ρ : SmoothCutoff) : ∃ (CD : ℝ), 0 < CD ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∀ (α β : Z4), ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 * ((1 + paperModeNormSq (k + α))⁻¹ ^ 2 * (1 + paperModeNormSq (k + β))⁻¹ ^ 2) ≤ CD * (1 + paperModeNormSq (α - β))⁻¹ ^ 2 * |Real.log ε|

Decay-retaining shifted window. When both quartic brackets are present, the window keeps the separation of the two centers: Σ_k ‖ρ̂(εk)‖²⟨k+α⟩⁻⁴⟨k+β⟩⁻⁴ ≤ C(ρ)·⟨α-β⟩⁻⁴·|log ε|, in the sharp multiplicative form.