Spare cutoff decay in the high-frequency R-324 branch

Paper Section 4.2, Step 4 only records the eighth-order central-frequency payoff. The selected noise mode is in fact larger than the target scale by a factor of order ε⁻¹/². Using twelfth-order Schwartz decay therefore leaves an additional factor ε⁴.

This slack is kept explicit here. It can pay a polynomial cell-scale cost inside a one-open-edge primitive estimate without consuming the separate ε⁻⁸ budget attached to the four external endpoint integrations.

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

The routed cutoff frequency controls ε² L with the stronger sqrt ε factor retained.

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

Twelfth-order cutoff decay yields the paper's eighth-order routed decay together with an explicit spare factor ε⁴.

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

The selected cutoff symbol has an ε⁴ reserve on the genuinely large central-frequency branch 1 ≤ ε² L.

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

Covariance-mode form of the same spare ε⁴ payoff, including the fixed white-noise half-density normalization.