Concrete construction of the refined R-324 routing data

This module removes the remaining global exact-sum obligation from the refined routing interface. It proves directly that the deterministic pairing sum is the finite sum of the actual residual-refined physical integrals. A caller then supplies only the configuration expansion and the corresponding per-fibre Fubini exchange.

Actual residual-refined physical integrals

noncomputable def Anderson4D.r324RefinedPhysicalIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (p : R324RefinedScheduleIndex m) : ℂ

Product-space integral of one genuine residual-refined fibre.

Equations

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

theorem Anderson4D.integrable_r324RefinedPhysicalIntegrand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (p : R324RefinedScheduleIndex m) : MeasureTheory.Integrable (r324Flatten (momentRefinedPhysicalIntegrand ρ ε m α β ↑p.fst ↑p.snd)) (r324PhysicalMeasure m)

theorem Anderson4D.r324RefinedPhysicalIntegral_eq_sum_contractionTerms (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (p : R324RefinedScheduleIndex m) : r324RefinedPhysicalIntegral ρ ε m α β p = ∑ e ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd, deterministicMomentContractionTerm ρ ε m α β e

One refined physical integral is exactly the finite contraction sum in that refined fibre.

theorem Anderson4D.sum_r324RefinedPhysicalIntegral_eq_contractionTerms (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) : ∑ p : R324RefinedScheduleIndex m, r324RefinedPhysicalIntegral ρ ε m α β p = ∑ e : MomentContraction m, deterministicMomentContractionTerm ρ ε m α β e

Summing the actual refined physical integrals over the genuine schedule subtype recovers the complete contraction sum exactly.

theorem Anderson4D.deterministicMomentPairingSum_eq_sum_refinedPhysicalIntegral (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) : deterministicMomentPairingSum ρ lam ε m α β = ↑(lamEps lam ε) ^ (2 * m) * ∑ p : R324RefinedScheduleIndex m, r324RefinedPhysicalIntegral ρ ε m α β p

Deterministic pairing sum as the finite refined-schedule integral, with the common coupling factor still outside.

Canonical representative and per-fibre expansion data

noncomputable def Anderson4D.r324RefinedScheduleRepresentative {m : ℕ} (p : R324RefinedScheduleIndex m) : MomentContraction m

Canonical representative used by the concrete grouped core.

Equations

• Anderson4D.r324RefinedScheduleRepresentative p = Classical.choose ⋯

theorem Anderson4D.r324RefinedScheduleRepresentative_mem {m : ℕ} (p : R324RefinedScheduleIndex m) : r324RefinedScheduleRepresentative p ∈ momentContractionFiber m ↑p.fst

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

Concrete configuration expansion of every actual refined core.

The only analytic equality requested from the caller is local to one refined fibre: its physical integral equals the tsum of the endpoint-first configuration terms. The global pairing-sum equality is proved in this module.

• 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) (r324RefinedScheduleRepresentative p) v = ∑' (a : ℕ), self.core p a v
• refinedIntegral_eq_tsum (p : R324RefinedScheduleIndex m) : ↑(lamEps lam ε) ^ (2 * m) * r324RefinedPhysicalIntegral ρ ε m α β p = ∑' (a : ℕ), r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p) (self.core p a)
• summable_term : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative 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.R324ConcreteRefinedCoreExpansion.toRefinedFourierRoutingData {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {hm : 0 < m} {α β : Z4} (d : R324ConcreteRefinedCoreExpansion ρ lam ε m hm α β) (hε : 0 < ε) (hε1 : ε ≤ 1) : R324RefinedFourierRoutingData ρ lam ε m hm α β

The local refined-core expansion automatically supplies the exact global routing data.

Equations

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