The very-high-frequency residue via the routed-key pigeonhole

This file closes R324VeryHighCentralFrequencySignedBound from the proved corrected route decomposition, leaving only a scalar route weight ledger.

The mechanism is the frequency-conservation pigeonhole at the routed scale: every countable central routed decomposition (CountableCentralRoutedMomentDecomposition) carries, per term, at most truncOrder ε increments summing exactly to freq(α+β), so one increment has norm at least ‖freq(α+β)‖ / truncOrder ε and the proved per-key covariance symbol decay term_le_increment_decay yields the routed decay unit ⟨‖freq(α+β)‖ / truncOrder ε⟩⁻⁸ directly — the exact bracket demanded by R324SignedCentralDecayBudget at the maximal admissible increment count nInc = truncOrder ε. No scale conversion through the weaker ⟨ε²(α+β)⟩⁻⁸ bracket is used, so no decay is discarded.

Instantiated on the corrected endpoint-nonzero route decomposition (countableCentralRoutedMomentReductionOutput_of_nonzeroRoutes), whose weights already carry the factor 16⟨α⟩⁻⁴⟨β⟩⁻⁴, the very-high residue follows from the single scalar ledger ∑' routes weight ≤ ⟨α⟩⁻⁴⟨β⟩⁻⁴ · B with ε⁸ · B ≤ amplitude: the paper's ε⁻⁸ endpoint sacrifice is borrowed entirely by the ledger.

theorem Anderson4D.r324VHF_exists_norm_sum_le_card_mul_norm {N : ℕ} (hN : 0 < N) (v : Fin N → EuclideanSpace ℝ (Fin dim)) : ∃ (i : Fin N), ‖∑ j : Fin N, v j‖ ≤ ↑N * ‖v i‖

Norm pigeonhole. Among finitely many Euclidean increments, one carries at least the average of their sum's norm.

theorem Anderson4D.r324VHF_norm_deterministicMomentPairingSum_le_of_countableRouted {ρ : SmoothCutoff} {lam ε weightBudget : ℝ} {m : ℕ} {α β : Z4} (htrunc : 1 ≤ truncOrder ε) (hred : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ weightBudget * eighthOrderFrequencyDecay ((↑(truncOrder ε))⁻¹ * ‖z4EuclideanFrequency (α + β)‖)

Routed-scale pigeonhole payoff. Any countable central routed decomposition of the deterministic moment obeys the eighth-order decay unit at the maximal routed increment scale ‖freq(α+β)‖ / truncOrder ε: per term, one of its at most truncOrder ε conserved increments is at least the routed average, and the per-key decay field converts it.

theorem Anderson4D.r324VHF_signedCentralDecayBudget_of_countableRouted {ρ : SmoothCutoff} {lam ε weightBudget amplitude : ℝ} {m : ℕ} {α β : Z4} (htrunc : 1 ≤ truncOrder ε) (hW : weightBudget ≤ amplitude * r324EndpointLoss ε α β) (hred : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β weightBudget) : R324SignedCentralDecayBudget ρ lam ε m α β amplitude

The signed central-decay budget from a routed weight budget. Any countable central routed decomposition whose total weight is at most amplitude · ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴ discharges the budget at nInc = truncOrder ε.

theorem Anderson4D.r324VeryHighCentralFrequencySignedBound_of_routeWeightLedger {ρ : SmoothCutoff} {lam ε amplitude B : ℝ} {m : ℕ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (hledger : ∀ (α β : Z4) (hexternal : α + β ≠ 0), ∑' (pr : R324RefinedScheduleIndex m × SmoothCutoff.R324NonzeroRouteLabel m), ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2 ≤ paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * B) (hAmp : ε ^ 8 * B ≤ amplitude) : R324VeryHighCentralFrequencySignedBound ρ lam ε m amplitude

The very-high-frequency residue from the corrected route weight ledger. For central frequencies above truncOrder ε · ε⁻¹ (indeed for every nonzero central frequency), the signed central-decay budget follows from the corrected endpoint-nonzero route decomposition and a single scalar ledger: the total route weight is at most ⟨α⟩⁻⁴⟨β⟩⁻⁴ · B with ε⁸ · B ≤ amplitude. The ε⁻⁸ endpoint sacrifice of the budget is thus borrowed entirely by the route mass B; the covariance-key decay itself is supplied by the proved per-key field of the route decomposition through the pigeonhole at the routed scale ‖freq(α+β)‖ / truncOrder ε.

Aggregate discharge of the route weight ledger

noncomputable def Anderson4D.r324VHFRawRouteMass (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) : ℝ

The α,β-independent raw route mass: the complete degree-eight raw covariance route series, summed over the refined schedule set.

Equations

• Anderson4D.r324VHFRawRouteMass ρ hm ε = ∑ p : Anderson4D.R324RefinedScheduleIndex m, ∑' (a : ℕ), ρ.r324RefinedRawCovarianceRouteWeight hm ε p a

theorem Anderson4D.r324VHFRawRouteMass_nonneg (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) : 0 ≤ r324VHFRawRouteMass ρ hm ε

theorem Anderson4D.r324VHF_tsum_routeWeight_le_modeDecay_mul_rawMass (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : ∑' (pr : R324RefinedScheduleIndex m × SmoothCutoff.R324NonzeroRouteLabel m), ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc pr.1 pr.2 ≤ paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * (16 * |lamEps lam ε| ^ (2 * m) * (SmoothCutoff.r324AllContractionInteriorSkeletonL1 m * r324VHFRawRouteMass ρ hm ε))

Aggregate route weight ledger. The total corrected route weight at fixed external modes is at most ⟨α⟩⁻⁴⟨β⟩⁻⁴ times the α,β-independent raw route mass ledger.

theorem Anderson4D.r324VeryHighCentralFrequencySignedBound_of_rawRouteMass {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (hAmp : ε ^ 8 * (16 * |lamEps lam ε| ^ (2 * m) * (SmoothCutoff.r324AllContractionInteriorSkeletonL1 m * r324VHFRawRouteMass ρ hm ε)) ≤ amplitude) : R324VeryHighCentralFrequencySignedBound ρ lam ε m amplitude

The very-high-frequency residue from one proved numeric ledger. R324VeryHighCentralFrequencySignedBound holds as soon as the raw route mass, at the paper's borrowed ε⁻⁸ endpoint sacrifice, fits under the amplitude: ε⁸ · 16 · |λ_ε|^{2m} · skeletonL1(m) · rawRouteMass ≤ amplitude.