Frequency-routing closure for R-324

This file contains the final assembly tools for paper §4.2 Step 4. The projected-noise construction and its covariance expansion are developed separately from the primitive-block iteration; this module joins their outputs at the RoutedMomentReductionOutput boundary.

structure Anderson4D.CountableCentralRoutedMomentDecomposition (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (weightBudget : ℝ) : Type

Paper-faithful countable version of the central-frequency part of the Step 4 decomposition.

The Fourier expansion of a projected mollified noise is a tsum, not a finite sum. Indexing by ℕ allows any countable frequency configuration to be enumerated (with zero padding).

This structure deliberately carries only the α+β decay. The α/β endpoint factors use the class-E cancellation after summing a whole primitive fiber, so imposing them term-by-term on Fourier configurations would be stronger than the paper.

• term : ℕ → ℂ
• weight : ℕ → ℝ
• incrementCount : ℕ → ℕ
• increment (a : ℕ) : Fin (self.incrementCount a) → EuclideanSpace ℝ (Fin dim)
• sum_eq : deterministicMomentPairingSum ρ lam ε m α β = ∑' (a : ℕ), self.term a
• summable_term : Summable self.term
• summable_weight : Summable self.weight
• weight_nonneg (a : ℕ) : 0 ≤ self.weight a
• incrementCount_pos (a : ℕ) : 0 < self.incrementCount a
• incrementCount_le_trunc (a : ℕ) : self.incrementCount a ≤ truncOrder ε
• increment_sum (a : ℕ) : ∑ i : Fin (self.incrementCount a), self.increment a i = z4EuclideanFrequency (α + β)
• term_le_increment_decay (a : ℕ) (i : Fin (self.incrementCount a)) : ‖self.term a‖ ≤ self.weight a * eighthOrderFrequencyDecay ‖self.increment a i‖
• tsum_weight_le : ∑' (a : ℕ), self.weight a ≤ weightBudget

def Anderson4D.CountableCentralRoutedMomentReductionOutput (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (weightBudget : ℝ) : Prop

Existence wrapper for the countable Fourier-configuration decomposition.

Equations

• Anderson4D.CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget = Nonempty (Anderson4D.CountableCentralRoutedMomentDecomposition ρ lam ε m α β weightBudget)

theorem Anderson4D.CountableCentralRoutedMomentReductionOutput.mono {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {weightBudget weightBudget' : ℝ} (h : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget) (hbudget : weightBudget ≤ weightBudget') : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget'

Countable routed decompositions are monotone in their total weight budget.

theorem Anderson4D.deterministicMomentPairingSum_centralDecay_bound_of_countableRoutedReduction {ρ : SmoothCutoff} {lam ε weightBudget : ℝ} {m : ℕ} {α β : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hred : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ weightBudget * eighthOrderFrequencyDecay (ε ^ 2 * ‖z4EuclideanFrequency (α + β)‖)

The countable Fourier decomposition and truncation-length routing give the central ⟨ε²(α+β)⟩⁻⁸ factor.

noncomputable def Anderson4D.r324EndpointLoss (ε : ℝ) (α β : Z4) : ℝ

The endpoint part of paper Step 4: four external Green integrations give the two fourth-order mode decays at the cost ε⁻⁸.

Equations

• Anderson4D.r324EndpointLoss ε α β = ε⁻¹ ^ 8 * Anderson4D.paperFourthOrderModeDecay α * Anderson4D.paperFourthOrderModeDecay β

theorem Anderson4D.r324EndpointLoss_nonneg (ε : ℝ) (α β : Z4) : 0 ≤ r324EndpointLoss ε α β

theorem Anderson4D.paperDeterministicMomentDecay_eq_endpoint_mul_central (ε : ℝ) (α β : Z4) : paperDeterministicMomentDecay ε α β = r324EndpointLoss ε α β * eighthOrderFrequencyDecay (ε ^ 2 * ‖z4EuclideanFrequency (α + β)‖)

theorem Anderson4D.deterministicMomentPairingSum_paperDecay_bound_of_countableCentralRouting {ρ : SmoothCutoff} {lam ε weightBudget amplitude : ℝ} {m : ℕ} {α β : Z4} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hred : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget) (hendpoint : weightBudget ≤ amplitude * r324EndpointLoss ε α β) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ amplitude * paperDeterministicMomentDecay ε α β

Combine a central countable routing output with the separate fiber-level endpoint-oscillation budget. The endpoint inequality is aggregate, so the class-E cancellation is not incorrectly imposed on individual Fourier configurations.

theorem Anderson4D.RoutedMomentReductionOutput.mono {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {amplitude amplitude' : ℝ} (h : RoutedMomentReductionOutput ρ lam ε m α β amplitude) (hamp : amplitude ≤ amplitude') : RoutedMomentReductionOutput ρ lam ε m α β amplitude'

A routed decomposition is monotone in its total weight budget. This is the bookkeeping needed to replace the independently selected uniform and routing constants by their maximum.

theorem Anderson4D.RoutedMomentReductionOutput.mono_max_left {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {amplitude extra : ℝ} (h : RoutedMomentReductionOutput ρ lam ε m α β amplitude) : RoutedMomentReductionOutput ρ lam ε m α β (max amplitude extra)

In particular, a routing constant can always be enlarged to the maximum of itself and an independently chosen uniform constant.