Residual-refined countable routing for R-324

The raw full-pairing Fourier series cannot be bounded termwise without losing the primitive-pairing cancellation. This file therefore indexes the final countable series by a genuine residual-refined schedule. Every configuration core contains the compatible primitive fibre sum before the four endpoint variables are integrated and before a norm is taken.

The data structure below records exact expansion and Fubini identities, not the target estimate. A separate constructor turns a proved local configuration estimate into the concrete CountableCentralRoutedMomentReductionOutput; its total endpoint budget is derived from summability and the explicit endpoint loss.

Finite residual-refined schedules

@[reducible, inline]

abbrev Anderson4D.R324RefinedScheduleIndex (m : ℕ) : Type

One actually realized within-half signature together with one actually realized residual-chain signature in its fibre.

Equations

• Anderson4D.R324RefinedScheduleIndex m = ((s : ↥(Anderson4D.momentContractionSignatures m)) × ↥(Anderson4D.momentResidualChainSignaturesAt m ↑s))

def Anderson4D.r324CanonicalRefinedSchedule (m : ℕ) : R324RefinedScheduleIndex m

Canonical refined schedule, used only to witness nonemptiness of the finite outer index.

Equations

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

instance Anderson4D.instNonemptyR324RefinedScheduleIndex (m : ℕ) : Nonempty (R324RefinedScheduleIndex m)

noncomputable def Anderson4D.r324NatEquivRefinedScheduleConfigurations (m : ℕ) : ℕ ≃ R324RefinedScheduleIndex m × ℕ

Exact flattening of the finite refined-schedule index and the natural-number configuration index.

Equations

• Anderson4D.r324NatEquivRefinedScheduleConfigurations m = (Denumerable.eqv (Anderson4D.R324RefinedScheduleIndex m × ℕ)).symm

Genuine grouped endpoint terms

noncomputable def Anderson4D.r324GroupedEndpointConfigurationTerm {m : ℕ} (hm : 0 < m) (_ρ : SmoothCutoff) (lam ε : ℝ) (α β : Z4) (e : MomentContraction m) (core : (Fin (2 * m) → T4) → ℂ) : ℂ

One residual-refined configuration after the four external Fourier integrations, followed by integration of all internal variables. The configuration core is a function of the doubled internal tuple and may already contain the complete compatible primitive-pairing fibre sum.

Equations

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

structure Anderson4D.R324RefinedFourierRoutingData (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) : Type

Exact, checkable analytic data at the residual-refined boundary.

core_tsum_eq ties the configuration series to the actual grouped core produced by momentRefinedPhysicalIntegrand_eq_endpointSeparated. sum_eq and summable_term are the Fubini/reindexing certificates; no decay estimate or target budget is included in this structure.

• representative : R324RefinedScheduleIndex m → MomentContraction m
• representative_mem (p : R324RefinedScheduleIndex m) : self.representative p ∈ momentContractionFiber m ↑p.fst
• core : R324RefinedScheduleIndex m → ℕ → (Fin (2 * m) → T4) → ℂ
• summable_core (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : Summable fun (a : ℕ) => self.core p a v
• core_tsum_eq (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : r324RefinedEndpointCore ρ ε m (↑p.fst) (↑p.snd) (self.representative p) v = ∑' (a : ℕ), self.core p a v
• sum_eq : deterministicMomentPairingSum ρ lam ε m α β = ∑' (p : R324RefinedScheduleIndex m × ℕ), r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (self.representative p.1) (self.core p.1 p.2)
• summable_term : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (self.representative p.1) (self.core p.1 p.2)
• incrementCount : R324RefinedScheduleIndex m × ℕ → ℕ
• increment (p : R324RefinedScheduleIndex m × ℕ) : Fin (self.incrementCount p) → EuclideanSpace ℝ (Fin dim)
• incrementCount_pos (p : R324RefinedScheduleIndex m × ℕ) : 0 < self.incrementCount p
• incrementCount_le_trunc (p : R324RefinedScheduleIndex m × ℕ) : self.incrementCount p ≤ truncOrder ε
• increment_sum (p : R324RefinedScheduleIndex m × ℕ) : ∑ i : Fin (self.incrementCount p), self.increment p i = z4EuclideanFrequency (α + β)

noncomputable def Anderson4D.R324RefinedFourierRoutingData.natTerm {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (d : R324RefinedFourierRoutingData ρ lam ε m hm α β) (a : ℕ) : ℂ

Natural-number flattened grouped term.

Equations

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

noncomputable def Anderson4D.R324RefinedFourierRoutingData.natIncrementCount {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (d : R324RefinedFourierRoutingData ρ lam ε m hm α β) (a : ℕ) : ℕ

Natural-number flattened increment count.

Equations

• d.natIncrementCount a = d.incrementCount ((Anderson4D.r324NatEquivRefinedScheduleConfigurations m) a)

noncomputable def Anderson4D.R324RefinedFourierRoutingData.natIncrement {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (d : R324RefinedFourierRoutingData ρ lam ε m hm α β) (a : ℕ) (i : Fin (d.natIncrementCount a)) : EuclideanSpace ℝ (Fin dim)

Natural-number flattened routed increments.

Equations

• d.natIncrement a i = d.increment ((Anderson4D.r324NatEquivRefinedScheduleConfigurations m) a) i

noncomputable def Anderson4D.R324RefinedFourierRoutingData.natWeight {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (_d : R324RefinedFourierRoutingData ρ lam ε m hm α β) (baseWeight : R324RefinedScheduleIndex m × ℕ → ℝ) (a : ℕ) : ℝ

Endpoint-weighted natural-number route weight. The factor 16 and the full r324EndpointLoss are explicit and are not assumptions.

Equations

• _d.natWeight baseWeight a = 16 * Anderson4D.r324EndpointLoss ε α β * baseWeight ((Anderson4D.r324NatEquivRefinedScheduleConfigurations m) a)

theorem Anderson4D.R324RefinedFourierRoutingData.toCountableCentralRoutedMomentReductionOutput {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (d : R324RefinedFourierRoutingData ρ lam ε m hm α β) (baseWeight : R324RefinedScheduleIndex m × ℕ → ℝ) (amplitude : ℝ) (hbaseSummable : Summable baseWeight) (hbaseNonneg : ∀ (p : R324RefinedScheduleIndex m × ℕ), 0 ≤ baseWeight p) (hbaseBudget : ∑' (p : R324RefinedScheduleIndex m × ℕ), baseWeight p ≤ amplitude) (hterm : ∀ (p : R324RefinedScheduleIndex m × ℕ) (i : Fin (d.incrementCount p)), ‖r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (d.representative p.1) (d.core p.1 p.2)‖ ≤ 16 * r324EndpointLoss ε α β * baseWeight p * eighthOrderFrequencyDecay ‖d.increment p i‖) : CountableCentralRoutedMomentReductionOutput ρ lam ε m α β (16 * amplitude * r324EndpointLoss ε α β)

A proved local grouped-configuration estimate and a summable endpoint-free core budget produce the concrete countable central routing output. The global endpoint budget is derived here.