A single projected residual covariance slot for R-324

This file isolates the safe algebraic and counting part of paper Section 4.2, Step 4.

The residual covariance slots are the cross-copy factors already present in momentCrossCovarianceProduct. A single marked slot is replaced by r324ProjectedCovarianceC; every other slot remains the complete spatial covariance etaEpsT4. In particular, this file never replaces the whole covariance product by a configuration in which every Fourier mode is fixed.

There is intentionally no theorem here identifying the original R-324 moment with the single-projected series. That later bridge must be proved from the post-phase-A residual expansion and its frequency-conservation identity. The declarations below provide only:

• the exact first large-increment selector;
• its coverage of every routed nonzero configuration;
• the concrete one-slot covariance replacement; and
• the triangle/counting bound for an already constructed summable family of one-slot projected terms.

The first large increment

noncomputable def Anderson4D.r324LargeResidualIncrementSlots {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (ε : ℝ) (δ : Fin N → E) : Finset (Fin N)

The slots which meet the truncation-scale routing threshold.

Equations

• Anderson4D.r324LargeResidualIncrementSlots ε δ = {i : Fin N | √ε / 2 * ‖∑ j : Fin N, δ j‖ ≤ ‖δ i‖}

theorem Anderson4D.r324LargeResidualIncrementSlots_nonempty {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) : (r324LargeResidualIncrementSlots ε δ).Nonempty

At least one slot meets the truncation-scale threshold.

noncomputable def Anderson4D.r324FirstLargeResidualIncrementSlot {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) : Fin N

The canonical routed slot is the least slot satisfying the large increment condition. Choosing the least slot makes the later fibres disjoint and avoids paying for the same configuration more than once.

Equations

• Anderson4D.r324FirstLargeResidualIncrementSlot hN δ hε hε1 hNtrunc = (Anderson4D.r324LargeResidualIncrementSlots ε δ).min' ⋯

theorem Anderson4D.r324FirstLargeResidualIncrementSlot_mem {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) : r324FirstLargeResidualIncrementSlot hN δ hε hε1 hNtrunc ∈ r324LargeResidualIncrementSlots ε δ

theorem Anderson4D.r324FirstLargeResidualIncrementSlot_spec {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) : √ε / 2 * ‖∑ j : Fin N, δ j‖ ≤ ‖δ (r324FirstLargeResidualIncrementSlot hN δ hε hε1 hNtrunc)‖

The selected slot has the required large increment.

theorem Anderson4D.r324FirstLargeResidualIncrementSlot_le {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) (i : Fin N) (hi : √ε / 2 * ‖∑ j : Fin N, δ j‖ ≤ ‖δ i‖) : r324FirstLargeResidualIncrementSlot hN δ hε hε1 hNtrunc ≤ i

The selector really is the first large slot.

theorem Anderson4D.r324FirstLargeResidualIncrementSlot_spec_of_sum {E : Type u_1} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (δ : Fin N → E) (external : E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) (hsum : ∑ j : Fin N, δ j = external) : √ε / 2 * ‖external‖ ≤ ‖δ (r324FirstLargeResidualIncrementSlot hN δ hε hε1 hNtrunc)‖

Frequency conservation rewrites the selected-slot bound in terms of the external shift.

@[reducible, inline]

abbrev Anderson4D.R324NonzeroResidualConfiguration {Ω : Type u_1} (term : Ω → ℂ) : Type u_1

The configurations relevant to a routed series.

Equations

• Anderson4D.R324NonzeroResidualConfiguration term = { ω : Ω // term ω ≠ 0 }

theorem Anderson4D.r324NonzeroResidualConfiguration_selectedSlot_spec {E : Type u_1} {Ω : Type u_2} [SeminormedAddCommGroup E] {N : ℕ} (hN : 0 < N) (term : Ω → ℂ) (increment : Ω → Fin N → E) (external : E) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hNtrunc : N ≤ truncOrder ε) (hsum : ∀ (ω : Ω), ∑ j : Fin N, increment ω j = external) (ω : R324NonzeroResidualConfiguration term) : √ε / 2 * ‖external‖ ≤ ‖increment (↑ω) (r324FirstLargeResidualIncrementSlot hN (increment ↑ω) hε hε1 hNtrunc)‖

Every nonzero routed configuration is covered by its canonical selected slot. The statement is stronger than needed analytically: the selector exists for zero terms too, but the subtype records the exact consumer boundary.

The existing residual covariance slots

@[reducible, inline]

abbrev Anderson4D.R324ResidualCovarianceSlot {m : ℕ} (κp : PartialPairing (Fin m)) : Type

After the within-half phase-A collapses, the remaining covariance slots are indexed by the left singles and paired across the cut by π.

Equations

• Anderson4D.R324ResidualCovarianceSlot κp = ↥κp.singles

noncomputable def Anderson4D.r324ResidualCovarianceSlotEquiv {m : ℕ} (κp : PartialPairing (Fin m)) : Fin κp.singles.card ≃ R324ResidualCovarianceSlot κp

Standard finite enumeration of the residual cross-covariance slots.

Equations

• Anderson4D.r324ResidualCovarianceSlotEquiv κp = κp.singles.equivFin.symm

theorem Anderson4D.card_r324ResidualCovarianceSlot {m : ℕ} (κp : PartialPairing (Fin m)) : Fintype.card (R324ResidualCovarianceSlot κp) = κp.singles.card

theorem Anderson4D.card_r324ResidualCovarianceSlot_le {m : ℕ} (κp : PartialPairing (Fin m)) : Fintype.card (R324ResidualCovarianceSlot κp) ≤ m

There are at most m residual covariance slots.

noncomputable def Anderson4D.r324ResidualCovarianceDisplacement {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (i : R324ResidualCovarianceSlot κp) : T4

Spatial displacement carried by one residual cross covariance.

Equations

• Anderson4D.r324ResidualCovarianceDisplacement κp κm π v i = v (Anderson4D.leftMomentIndex ↑i) - v (Anderson4D.rightMomentIndex ↑(π i))

noncomputable def Anderson4D.SmoothCutoff.r324SingleProjectedResidualCovarianceFactor {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (selected i : R324ResidualCovarianceSlot κp) : ℂ

Replace exactly one residual covariance factor by its high-frequency projection. Every unselected factor is literally the complete etaEpsT4 covariance.

Equations

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

@[simp]

theorem Anderson4D.SmoothCutoff.r324SingleProjectedResidualCovarianceFactor_selected {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (selected : R324ResidualCovarianceSlot κp) : ρ.r324SingleProjectedResidualCovarianceFactor ε L κp κm π v selected selected = ρ.r324ProjectedCovarianceC ε L (r324ResidualCovarianceDisplacement κp κm π v selected)

@[simp]

theorem Anderson4D.SmoothCutoff.r324SingleProjectedResidualCovarianceFactor_other {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (selected i : R324ResidualCovarianceSlot κp) (hi : i ≠ selected) : ρ.r324SingleProjectedResidualCovarianceFactor ε L κp κm π v selected i = ↑(ρ.etaEpsT4 ε (r324ResidualCovarianceDisplacement κp κm π v i))

noncomputable def Anderson4D.SmoothCutoff.r324SingleProjectedResidualCovarianceProduct {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (selected : R324ResidualCovarianceSlot κp) : ℂ

The residual product with one and only one projected covariance.

Equations

• ρ.r324SingleProjectedResidualCovarianceProduct ε L κp κm π v selected = ∏ i : Anderson4D.R324ResidualCovarianceSlot κp, ρ.r324SingleProjectedResidualCovarianceFactor ε L κp κm π v selected i

theorem Anderson4D.SmoothCutoff.r324SingleProjectedResidualCovarianceProduct_eq {m : ℕ} (ρ : SmoothCutoff) (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (selected : R324ResidualCovarianceSlot κp) : ρ.r324SingleProjectedResidualCovarianceProduct ε L κp κm π v selected = ρ.r324ProjectedCovarianceC ε L (r324ResidualCovarianceDisplacement κp κm π v selected) * ∏ i ∈ Finset.univ.erase selected, ↑(ρ.etaEpsT4 ε (r324ResidualCovarianceDisplacement κp κm π v i))

Explicit factorization: the selected projected covariance times the product of all complete unselected etaEpsT4 factors.

Countable grouping by the single selected slot

noncomputable def Anderson4D.r324SingleProjectedSlotMass {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (selected : Ω → ι) (term : Ω → ℂ) (i : ι) : ℝ

Absolute mass of the fibre whose canonical projected slot is i.

Equations

• Anderson4D.r324SingleProjectedSlotMass selected term i = ∑' (ω : ↑(selected ⁻¹' {i})), ‖term ↑ω‖

theorem Anderson4D.r324SingleProjectedSlotMass_nonneg {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (selected : Ω → ι) (term : Ω → ℂ) (i : ι) : 0 ≤ r324SingleProjectedSlotMass selected term i

theorem Anderson4D.norm_tsum_le_sum_singleProjectedSlotMass {Ω : Type u_1} {ι : Type u_2} [Fintype ι] (selected : Ω → ι) (term : Ω → ℂ) (hterm : Summable term) : ‖∑' (ω : Ω), term ω‖ ≤ ∑ i : ι, r324SingleProjectedSlotMass selected term i

A summable family of already constructed one-slot projected terms costs only the finite sum over possible selected slots. The fibres are disjoint because selected is a function (in the routed application it is the least-large-increment selector above).

noncomputable def Anderson4D.SmoothCutoff.r324SingleProjectedResidualTerm {Ω : Type u_1} {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (L : Ω → ℝ) (v : Ω → Fin (2 * m) → T4) (amplitude : Ω → ℂ) (selected : Ω → R324ResidualCovarianceSlot κp) (ω : Ω) : ℂ

A concrete family in which each term has one projected residual covariance and all other residual covariances remain complete etaEpsT4 factors.

Equations

• ρ.r324SingleProjectedResidualTerm ε κp κm π L v amplitude selected ω = amplitude ω * ρ.r324SingleProjectedResidualCovarianceProduct ε (L ω) κp κm π (v ω) (selected ω)

theorem Anderson4D.SmoothCutoff.norm_tsum_r324SingleProjectedResidualTerm_le {Ω : Type u_1} {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (L : Ω → ℝ) (v : Ω → Fin (2 * m) → T4) (amplitude : Ω → ℂ) (selected : Ω → R324ResidualCovarianceSlot κp) (hterm : Summable (ρ.r324SingleProjectedResidualTerm ε κp κm π L v amplitude selected)) : ‖∑' (ω : Ω), ρ.r324SingleProjectedResidualTerm ε κp κm π L v amplitude selected ω‖ ≤ ∑ i : R324ResidualCovarianceSlot κp, r324SingleProjectedSlotMass selected (ρ.r324SingleProjectedResidualTerm ε κp κm π L v amplitude selected) i

The concrete single-projected residual series is bounded by a sum over at most κp.singles.card ≤ m slot fibres. This theorem does not claim that the original moment equals this series.