Shrinking the high-frequency residue (band closure)

The proved reduction leaves the signed central-decay budget open for all central frequencies ‖freq(α+β)‖ > ε⁻¹. This file closes the routed band ε⁻¹ < ‖freq(α+β)‖ ≤ truncOrder ε · ε⁻¹ unconditionally from the interior inserted-majorant estimate: at the maximal admissible increment count nInc = truncOrder ε the routed argument ‖freq‖/nInc is still below the covariance frequency ε⁻¹, so the routed decay unit is worth ε⁸/16 and the ε⁻⁸ endpoint sacrifice closes the budget inequality exactly as in the low regime.

Consequently the remaining high-frequency residue is only the very high regime ‖freq(α+β)‖ > truncOrder ε · ε⁻¹, where the covariance bracket satisfies ε‖freq‖ > ⌊|log ε|⌋ and the paper's rapid symbol decay first has genuine room.

theorem Anderson4D.signedCentralDecay_ineq_of_interiorCore_bandFrequency {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (hlog : 1 ≤ |Real.log ε|) (α β : Z4) (hcore : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) (hAmaj : 16 * (16 ^ (2 * m) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) ≤ amplitude) (hband : ‖z4EuclideanFrequency (α + β)‖ ≤ ↑(truncOrder ε) * ε⁻¹) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ amplitude * r324EndpointLoss ε α β * eighthOrderFrequencyDecay ((↑(truncOrder ε))⁻¹ * ‖z4EuclideanFrequency (α + β)‖)

Band closure of the signed budget. For central frequencies up to truncOrder ε · ε⁻¹ the routed decay unit at the maximal increment count nInc = truncOrder ε is still worth ε⁸/16, so the mode-decay aggregation and the ε⁻⁸ endpoint sacrifice close the budget inequality on the whole band.

def Anderson4D.R324VeryHighCentralFrequencySignedBound (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (amplitude : ℝ) : Prop

The very-high-frequency residue. Only central frequencies above truncOrder ε · ε⁻¹ remain: there the covariance-scale bracket satisfies ε‖freq(α+β)‖ > ⌊|log ε|⌋, the regime where the rapid decay of the covariance symbol first has genuine room. The band ε⁻¹ < ‖freq(α+β)‖ ≤ truncOrder ε · ε⁻¹ is discharged by signedCentralDecay_ineq_of_interiorCore_bandFrequency, so this Prop is strictly smaller than R324HighCentralFrequencySignedBound.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324VeryHighCentralFrequencySignedBound.mono {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {amplitude amplitude' : ℝ} (h : R324VeryHighCentralFrequencySignedBound ρ lam ε m amplitude) (hle : amplitude ≤ amplitude') : R324VeryHighCentralFrequencySignedBound ρ lam ε m amplitude'

The very-high residue is monotone in the amplitude.

theorem Anderson4D.r324HighCentralFrequencySignedBound_of_interiorCore_and_veryHigh {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (hlog : 1 ≤ |Real.log ε|) (hcore : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) (hAmaj : 16 * (16 ^ (2 * m) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) ≤ amplitude) (hveryhigh : R324VeryHighCentralFrequencySignedBound ρ lam ε m amplitude) : R324HighCentralFrequencySignedBound ρ lam ε m amplitude

Shrinking the high-frequency residue. The interior inserted-majorant estimate and its aggregated amplitude close the band ε⁻¹ < ‖freq(α+β)‖ ≤ truncOrder ε · ε⁻¹ with nInc = truncOrder ε, so the full high-frequency signed bound follows from the very-high residue alone.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_interiorCore_and_veryHighFrequency {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < m → 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant → R324VeryHighCentralFrequencySignedBound ρ lam ε m (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

The reduced final assembly at the very-high residue. The paper bound (3.24) in its frozen paperDeterministicMomentRHS shape at an ε-uniform outer constant follows from the interior inserted-majorant estimate together with only the very-high-frequency residue of the signed central-decay budget: central frequencies up to truncOrder ε · ε⁻¹ are closed unconditionally here.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_logBudget_and_veryHighFrequency {C supportConstant : ℝ} (hC : 0 < C) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < m → 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreLogBudget ρ ε m C → R324VeryHighCentralFrequencySignedBound ρ lam ε m (lamEps lam ε ^ 2 * outerConstant * (16 * (supportConstant / min supportConstant 1 ^ 2 * C) * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * (supportConstant / min supportConstant 1 ^ 2 * C)) lam ε m α β

The sharpened complete reduced form of the deterministic moment estimate. The paper bound (3.24) at ε-uniform constants follows from exactly two residual scalar statements: the ε-uniform interior-core logarithmic budget, and the signed bound at central frequencies above truncOrder ε · ε⁻¹ only. This strictly improves the proved reduction, whose second residue began at ε⁻¹.

theorem Anderson4D.exists_deterministicMoment_decay_bound_of_logBudget_and_veryHighFrequency {C supportConstant : ℝ} (hC : 0 < C) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < m → 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreLogBudget ρ ε m C → R324VeryHighCentralFrequencySignedBound ρ lam ε m (lamEps lam ε ^ 2 * outerConstant * (16 * (supportConstant / min supportConstant 1 ^ 2 * C) * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (16 * (supportConstant / min supportConstant 1 ^ 2 * C) * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Literal decay-bracket corollary of the sharpened reduction.