Frequency routing and endpoint oscillation (paper §4.2, Step 4)

This file isolates the deterministic inequalities used in the frequency-decay part of the proof of (3.24):

• if a composition of finitely many factors produces a total frequency shift, one factor carries at least the average shift;
• under a bound on the number of factors, this gives the ε^(1/2) L high-frequency factor singled out in the paper;
• the endpoint phase difference has both the global linear estimate and the even, quadratic cosine estimate used after the 𝓔-cancellation.

Keeping these statements independent of the parametrix syntax makes the frequency-routing step reusable when the closed deterministic profiles are assembled in Estimates.lean.

A large increment carries the total frequency shift

theorem Anderson4D.exists_large_frequency_increment {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) : ∃ (i : Fin N), ‖∑ j : Fin N, δ j‖ ≤ ↑N * ‖δ i‖

A finite sum in a seminormed group has a summand carrying at least its average norm. The division-free form is convenient for the paper's O(|log ε|) composition length.

theorem Anderson4D.exists_frequency_increment_above_threshold {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) (r : ℝ) (hr : 0 < r) (hcount : ↑N ≤ r⁻¹) : ∃ (i : Fin N), r * ‖∑ j : Fin N, δ j‖ ≤ ‖δ i‖

Threshold form of frequency routing. If the number of factors is at most r⁻¹, one factor shifts frequency by at least r times the total shift. In the paper one takes r = ε^(1/2).

theorem Anderson4D.exists_frequency_increment_above_sqrt {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) (ε : ℝ) (hε : 0 < ε) (hcount : ↑N ≤ (√ε)⁻¹) : ∃ (i : Fin N), √ε * ‖∑ j : Fin N, δ j‖ ≤ ‖δ i‖

The concrete square-root-scale version quoted in paper §4.2 Step 4. It is stated with sqrt ε, avoiding any ambiguity about real powers.

theorem Anderson4D.truncOrder_cast_le_two_mul_inv_sqrt {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : ↑(truncOrder ε) ≤ 2 * (√ε)⁻¹

The paper's truncation length is eventually much smaller than the inverse square-root scale. The explicit constant 2 follows directly from log x ≤ x^(1/2)/(1/2).

theorem Anderson4D.exists_frequency_increment_at_truncation_scale {E : Type u_1} [SeminormedAddCommGroup E] (N : ℕ) (hN : 0 < N) (δ : Fin N → E) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) : ∃ (i : Fin N), √ε / 2 * ‖∑ j : Fin N, δ j‖ ≤ ‖δ i‖

Concrete routing at the actual truncation order. A chain of at most A = floor |log ε| factors contains a shift of size at least (sqrt ε / 2) times the total shift. The absolute factor 2 is harmless in the multiplier decay and is now explicit rather than hidden by ≳.

The eighth-order multiplier payoff

noncomputable def Anderson4D.eighthOrderFrequencyDecay (x : ℝ) : ℝ

The paper's ⟨x⟩⁻⁸, written without real powers: (1 + x²)⁻⁴. This form has the same value and a simpler order API.

Equations

• Anderson4D.eighthOrderFrequencyDecay x = ((1 + x ^ 2) ^ 4)⁻¹

theorem Anderson4D.eighthOrderFrequencyDecay_nonneg (x : ℝ) : 0 ≤ eighthOrderFrequencyDecay x

theorem Anderson4D.eighthOrderFrequencyDecay_anti {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) : eighthOrderFrequencyDecay y ≤ eighthOrderFrequencyDecay x

⟨x⟩⁻⁸ is decreasing on the nonnegative half-line.

theorem Anderson4D.routed_decay_le_sqrt_decay {ε L h : ℝ} (_hε : 0 ≤ ε) (hL : 0 ≤ L) (hroute : √ε * L ≤ h) : eighthOrderFrequencyDecay h ≤ eighthOrderFrequencyDecay (√ε * L)

A routed shift of size sqrt ε · L supplies at least the decay at that scale.

theorem Anderson4D.sqrt_decay_le_eps_sq_decay {ε L : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 ≤ L) : eighthOrderFrequencyDecay (√ε * L) ≤ eighthOrderFrequencyDecay (ε ^ 2 * L)

For 0 < ε ≤ 1, the routed sqrt ε · L decay is stronger than the ε² L decay printed in (3.24). This is the precise scale comparison left implicit in paper §4.2 Step 4.

theorem Anderson4D.routed_decay_le_eps_sq_decay {ε L h : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hL : 0 ≤ L) (hroute : √ε * L ≤ h) : eighthOrderFrequencyDecay h ≤ eighthOrderFrequencyDecay (ε ^ 2 * L)

The complete scalar payoff of the routing argument: a selected high-frequency factor at sqrt ε · L yields the exact ⟨ε²L⟩⁻⁸ factor used in (3.24).

theorem Anderson4D.eps_sq_le_sqrt_div_two {ε : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) : ε ^ 2 ≤ √ε / 2

On the eventual range ε ≤ 1/4, the explicit factor 1/2 from the truncation-length routing still dominates the paper's ε² scale.

theorem Anderson4D.truncation_routed_decay_le_eps_sq_decay {ε L h : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hL : 0 ≤ L) (hroute : √ε / 2 * L ≤ h) : eighthOrderFrequencyDecay h ≤ eighthOrderFrequencyDecay (ε ^ 2 * L)

Exact decay payoff for a shift selected at the actual truncation order. This is the paper's Step 4 scale comparison with all eventual constants visible.

Endpoint oscillation

theorem Anderson4D.norm_complex_phase_sub_one_le (θ : ℝ) : ‖Complex.exp (Complex.I * ↑θ) - 1‖ ≤ |θ|

Global endpoint-phase estimate. This is the bound used before taking absolute values in the four external variables of (4.18).

theorem Anderson4D.abs_cos_sub_one_le_two (θ : ℝ) : |Real.cos θ - 1| ≤ 2

The global bounded estimate for the real endpoint oscillation.

theorem Anderson4D.abs_cos_sub_one_le_sq (θ : ℝ) : |Real.cos θ - 1| ≤ θ ^ 2

The quadratic endpoint estimate after the odd part has vanished by 𝓔-symmetry. The paper only needs the coarser constant 1; the elementary identity actually gives the sharper constant 1/2.

theorem Anderson4D.endpoint_oscillation_bounds (θ : ℝ) : |Real.cos θ - 1| ≤ θ ^ 2 ∧ |Real.cos θ - 1| ≤ 2

Both endpoint bounds in one interface. The assembly chooses the quadratic branch when the inserted diameter is available and the bounded branch when preserving Fourier decay costs the paper's ε⁻² loss.