The routed window values at low order

(D) The unconditional window side. The routed ledgers of R324RoutedWindowBudget measure each covariance pair against a lattice window. This file closes the value side of those ledgers at the orders the paper needs first:

• r324RoutedWindow_marked_window_le — the marked-slot window: one degree-eight routing cost (1+‖k‖²)⁴, damped by the single retained diagonal Green window ⟨k⟩⁻⁴, costs exactly the endpoint sacrifice: Σ_k (1+‖k‖²)⁴·⟨k⟩⁻⁴·‖ρ̂(εk)‖² ≤ C·ε⁻⁸. This is the factor the scalar raw ledger provably lost (ε⁻¹² without the window), and it is the per-marked-pair factor of the windowed value at every m;
• r324RoutedWindow_value_one / r324RoutedWindow_value_two — the m ≤ 2 windowed values in the exact C^m·L^{m-1}·ε⁻⁸ normal form of the routed Props: at m = 1 the marked window alone (no logarithm); at m = 2 the marked window times the decay-retaining separated window r324SW_separated_window_le_log, which slots into the cross pair and keeps the ⟨γ-δ⟩⁻⁴ separation of the two window centers.

The tail of the marked window needs symbol decay strictly beyond the proved degree-eight bound, so we first derive the degree-twelve scaled bound from the arbitrary-order rapid decay exists_fourierR4_one_add_norm_bound_nat 6.

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

Degree-six decay of the scaled symbol against the sup bracket, squared: the degree-twelve companion of r324SW_symbol_sq_le_of_decay_eight, needed because the marked slot retains a net fourth-order growth.

theorem Anderson4D.r324RoutedWindow_paperModeNormSq_le (k : Z4) : paperModeNormSq k ≤ 4 * ↑(z4SupRadius k) ^ 2

The Euclidean mode square is at most dim sup-radius squares.

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

The marked-slot window. One degree-eight routing cost, damped by the retained diagonal Green window, costs exactly the endpoint sacrifice ε⁻⁸ — not the raw ε⁻¹² of the windowless ledger: Σ_k (1+‖k‖²)⁴ ⟨k⟩⁻⁴ ‖ρ̂(εk)‖² ≤ CM·ε⁻⁸.

theorem Anderson4D.r324RoutedWindow_value_one (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∑' (k : Z4), (1 + ‖z4EuclideanFrequency k‖ ^ 2) ^ 4 * paperFourthOrderModeDecay k * ‖ρ.symbol ε k‖ ^ 2 ≤ C ^ 1 * |Real.log ε| ^ (1 - 1) * ε⁻¹ ^ 8

The order-one routed window value, in the exact C^m·L^{m-1}·ε⁻⁸ normal form of the routed Props: at m = 1 the marked window alone funds the budget and no logarithm is spent.

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

The order-two routed window value. The marked pair pays the endpoint sacrifice ε⁻⁸; the second (cross) pair is evaluated by the decay-retaining separated window, worth one logarithm and keeping the ⟨γ-δ⟩⁻⁴ separation of its two centers: the windowed pair-pattern value is C²·L^{2-1}·ε⁻⁸ with the separation retained as a bonus.