Concrete exact refined Fourier expansion

This module instantiates the exact structural fields of R324ConcreteRefinedCoreExpansion with the common-increment grouped cores. It contains no decay estimate and no target budget.

The raw series is the genuine refined physical integral

theorem Anderson4D.SmoothCutoff.tsum_r324RefinedRawEndpointCore (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (p : R324RefinedScheduleIndex m) (v : Fin (2 * m) → T4) : ∑' (a : ℕ), ρ.r324RefinedRawEndpointCore hm ε p a v = r324RefinedEndpointCore ρ ε m (↑p.fst) (↑p.snd) (r324RefinedScheduleRepresentative p) v

The raw endpoint cores sum exactly to the actual complete refined core.

theorem Anderson4D.SmoothCutoff.r324EndpointSeparatedIntegrand_tsum (α β : Z4) (anchors : R324EndpointAnchors) (flags : R324EndpointFlags) (core : ℕ → ℂ) (x y z w : T4) : r324EndpointSeparatedIntegrand α β anchors flags (∑' (a : ℕ), core a) x y z w = ∑' (a : ℕ), r324EndpointSeparatedIntegrand α β anchors flags (core a) x y z w

Endpoint separation commutes with an ordinary summable series of cores.

theorem Anderson4D.SmoothCutoff.momentRefinedPhysicalIntegrand_eq_rawEndpoint_tsum (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (x y z w : T4) (v : Fin (2 * m) → T4) : momentRefinedPhysicalIntegrand ρ ε m α β (↑p.fst) (↑p.snd) x y z w v = ∑' (a : ℕ), ρ.r324RefinedRawEndpointIntegrand hm ε α β p a x y z w v

The genuine refined physical integrand is pointwise the complete raw Fourier series.

theorem Anderson4D.SmoothCutoff.r324RefinedPhysicalIntegral_eq_rawFourier_tsum (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) : r324RefinedPhysicalIntegral ρ ε m α β p = ∑' (a : ℕ), ρ.r324RefinedRawFourierIntegral hm ε α β p a

The actual refined physical integral is exactly the raw refined Fourier-integral series.

Regrouping the exact integrated series

theorem Anderson4D.SmoothCutoff.summable_r324KeyGroupedEndpointConfigurationTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) : Summable fun (b : ℕ) => r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p b)

The grouped endpoint terms in one refined schedule are summable.

theorem Anderson4D.SmoothCutoff.r324RefinedPhysicalIntegral_eq_keyGroupedEndpoint_tsum (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) : ↑(lamEps lam ε) ^ (2 * m) * r324RefinedPhysicalIntegral ρ ε m α β p = ∑' (b : ℕ), r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p b)

Exact per-schedule Fubini/regrouping identity required by the concrete refined expansion structure.

Frequency conservation and the concrete structure

theorem Anderson4D.SmoothCutoff.r324RefinedRawFourierIntegral_eq_natFullPairingFourierTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) : ρ.r324RefinedRawFourierIntegral hm ε α β p a = have u := (r324NatEquivRefinedContractionConfigurations p) a; have κ := (momentContractionEquivFullPairing m) ↑u.1; ρ.r324NatFullPairingFourierTerm hm ε α β κ u.2

The raw refined integral is the existing natural full-pairing Fourier term selected by its decoded contraction/configuration.

theorem Anderson4D.SmoothCutoff.sum_r324RefinedRawIncrementKey_eq_external_of_ne_zero (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m) (a : ℕ) (hne : ρ.r324RefinedRawFourierIntegral hm ε α β p a ≠ 0) : ∑ i : Fin m, z4EuclideanFrequency (r324RefinedRawIncrementKey hm p a i) = z4EuclideanFrequency (α + β)

Every nonzero raw refined integral has the exact external increment sum.

theorem Anderson4D.SmoothCutoff.exists_rawFourierIntegral_ne_zero_of_grouped_ne_zero (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (hne : r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p b) ≠ 0) : ∃ (a : ℕ), r324RefinedRawIncrementKey hm p a = (r324NatEquivStandardConfigurations hm) b ∧ ρ.r324RefinedRawFourierIntegral hm ε α β p a ≠ 0

A nonzero grouped endpoint term contains a nonzero raw integral in its common-increment fibre.

theorem Anderson4D.SmoothCutoff.sum_keyGroupedIncrement_eq_external_of_ne_zero (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m) (b : ℕ) (hne : r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p b) ≠ 0) : ∑ i : Fin m, z4EuclideanFrequency ((r324NatEquivStandardConfigurations hm) b i) = z4EuclideanFrequency (α + β)

Every nonzero common-increment group has the exact external increment sum.

noncomputable def Anderson4D.SmoothCutoff.r324ConcreteRefinedIncrement (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) (i : Fin m) : EuclideanSpace ℝ (Fin dim)

Routed increment of one concrete group. Nonzero terms use their actual shared Fourier key. A zero term uses a harmless delta route so that frequency conservation remains unconditional.

Equations

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

theorem Anderson4D.SmoothCutoff.sum_r324ConcreteRefinedIncrement (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (p : R324RefinedScheduleIndex m × ℕ) : ∑ i : Fin m, ρ.r324ConcreteRefinedIncrement lam hm ε α β p i = z4EuclideanFrequency (α + β)

theorem Anderson4D.SmoothCutoff.summable_all_r324KeyGroupedEndpointConfigurationTerm (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) : Summable fun (p : R324RefinedScheduleIndex m × ℕ) => r324GroupedEndpointConfigurationTerm hm ρ lam ε α β (r324RefinedScheduleRepresentative p.1) (ρ.r324KeyGroupedRefinedEndpointCore hm ε p.1 p.2)

Summability over all refined schedules and grouped configurations.

noncomputable def Anderson4D.SmoothCutoff.r324ConcreteRefinedCoreExpansion (ρ : SmoothCutoff) (lam : ℝ) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hmtrunc : m ≤ truncOrder ε) (α β : Z4) : R324ConcreteRefinedCoreExpansion ρ lam ε m hm α β

Fully concrete exact refined Fourier expansion. The remaining primitive-collapse/local-decay estimate is deliberately not a field of this structure.

Equations

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