Selector-retaining regrouping by the paper's operator slot

Paper Section 4.2, Step 4(B) first chooses which factor in the operator composition carries the large frequency shift. The choice costs only the finite number of operator factors. It must happen before any norm is taken and before the complete primitive-pairing sum is split.

The corrected endpoint-nonzero route label contains much more data than that paper choice: it also fixes a contraction and a complete Fourier increment key. This file forgets those extra components only as a fibre map. Thus all contractions, increment keys and selector-restricted configurations with the same underlying operator position remain in one signed series.

No route norm and no entity norm occurs below. The sole triangle inequality is the finite one over Fin m, matching the paper's choice of one factor in a composition of length at most the truncation order.

The complete signed term on one corrected route

noncomputable def Anderson4D.SmoothCutoff.r324RefinedQuadOpenCovarianceRouteTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) : ℂ

The contribution of one corrected route to the open covariance series. The inner selector fibre is still summed before any norm is taken.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedQuadOpenCovarianceRouteTerm_eq_raw (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (route : R324NonzeroRouteLabel m) : ρ.r324RefinedQuadOpenCovarianceRouteTerm hm ε α β hexternal hε hε1 hmtrunc p route = ∑' (a : ρ.R324RefinedEndpointNonzeroRouteFiber hm ε α β hexternal hε hε1 hmtrunc p route), ρ.r324RefinedRawFullPairingIntegral hm ε α β p ↑↑a

Removing the selected covariance coefficient was an exact operation, so one open route term is exactly the corresponding signed raw route fibre.

theorem Anderson4D.SmoothCutoff.summable_r324RefinedQuadOpenCovarianceRouteTerm (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) : Summable fun (route : R324NonzeroRouteLabel m) => ρ.r324RefinedQuadOpenCovarianceRouteTerm hm ε α β hexternal hε hε1 hmtrunc p route

The complete route family is absolutely summable. This is inherited from the original raw Fourier expansion through exact fibrewise regrouping; it is not obtained by an analytic route budget.

Forget only to the operator position

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324RefinedQuadSelectedPositionRawFiber {m : ℕ} (ρ : SmoothCutoff) (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) : Type

Endpoint-nonzero raw configurations whose canonical first-large cross covariance has the same underlying position in the original m-factor operator composition. The contraction is deliberately not part of the outer index.

Equations

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

What "first" means: the ordered singles enumeration

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

Every slot strictly before the canonical first-large slot fails the large-increment predicate. The order here is the paper selector order on Fin N; it is not an order on the ambient physical positions.

theorem Anderson4D.SmoothCutoff.r324CrossPairMode_not_mem_high_before_firstLarge (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (j : Fin κp.singles.card) (hj : j < r324FirstLargeResidualIncrementSlot ⋯ (r324EnumeratedCrossSlotIncrement κp κm π ↑ω) hε hε1 ⋯) : ↑ω (r324CrossSlotPairIndex κp κm π ((r324ResidualCovarianceSlotEquiv κp) j)) ∉ r324HighModeSet ε ‖z4EuclideanFrequency (α + β)‖

On every earlier slot in the ordered singles enumeration, the actual cross-pair mode lies in the complementary low set. This is the missing "earlier factors low" half of the paper's first-large decomposition.

theorem Anderson4D.SmoothCutoff.r324LowCovarianceModeTerm_before_firstLarge_eq (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (j : Fin κp.singles.card) (hj : j < r324FirstLargeResidualIncrementSlot ⋯ (r324EnumeratedCrossSlotIncrement κp κm π ↑ω) hε hε1 ⋯) (z : T4) : ρ.r324LowCovarianceModeTerm ε ‖z4EuclideanFrequency (α + β)‖ z (↑ω (r324CrossSlotPairIndex κp κm π ((r324ResidualCovarianceSlotEquiv κp) j))) = ρ.r324CovarianceModeTerm ε z (↑ω (r324CrossSlotPairIndex κp κm π ((r324ResidualCovarianceSlotEquiv κp) j)))

Therefore every earlier cross-pair mode is retained, unchanged, by the low-mode indicator.

Paper Step 4(B): the first-high telescope itself

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

The full cross covariance in the canonical ordered-singles enumeration.

Equations

• ρ.r324EnumeratedCrossFullCovariance ε κp κm π v j = ↑(ρ.etaEpsT4 ε (Anderson4D.r324ResidualCovarianceDisplacement κp κm π v ((Anderson4D.r324ResidualCovarianceSlotEquiv κp) j)))

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

The low part of the same enumerated cross covariance.

Equations

• ρ.r324EnumeratedCrossLowCovariance ε L κp κm π v j = ρ.r324LowCovarianceC ε L (Anderson4D.r324ResidualCovarianceDisplacement κp κm π v ((Anderson4D.r324ResidualCovarianceSlotEquiv κp) j))

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

The high part of the same enumerated cross covariance.

Equations

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

theorem Anderson4D.SmoothCutoff.r324EnumeratedCrossFullCovariance_eq_low_add_high (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) (j : Fin κp.singles.card) : ρ.r324EnumeratedCrossFullCovariance ε κp κm π v j = ρ.r324EnumeratedCrossLowCovariance ε L κp κm π v j + ρ.r324EnumeratedCrossHighCovariance ε L κp κm π v j

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

The all-low term in the paper's exact telescope.

Equations

• ρ.r324AllLowCrossCovarianceProduct ε L κp κm π v = ∏ j : Fin κp.singles.card, ρ.r324EnumeratedCrossLowCovariance ε L κp κm π v j

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

The summand whose first high cross factor is selectedOrder: low before it, high at it, and full after it.

Equations

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

theorem Anderson4D.SmoothCutoff.prod_r324EnumeratedCrossFullCovariance_eq_allLow_add_firstHigh (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ∏ j : Fin κp.singles.card, ρ.r324EnumeratedCrossFullCovariance ε κp κm π v j = ρ.r324AllLowCrossCovarianceProduct ε L κp κm π v + ∑ selectedOrder : Fin κp.singles.card, ρ.r324FirstHighCrossCovarianceProduct ε L κp κm π v selectedOrder

This is exactly the already-proved generic first-high telescope, specialized to the paper's cross-covariance composition.

theorem Anderson4D.SmoothCutoff.coe_momentCrossCovarianceProduct_eq_enumerated (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ↑(momentCrossCovarianceProduct ρ ε m κp κm π v) = ∏ j : Fin κp.singles.card, ρ.r324EnumeratedCrossFullCovariance ε κp κm π v j

Reindexing by ordered singles identifies the paper telescope's full product with the actual cross-covariance product in (4.18).

theorem Anderson4D.SmoothCutoff.coe_momentCrossCovarianceProduct_eq_allLow_add_firstHigh (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : ↑(momentCrossCovarianceProduct ρ ε m κp κm π v) = ρ.r324AllLowCrossCovarianceProduct ε L κp κm π v + ∑ selectedOrder : Fin κp.singles.card, ρ.r324FirstHighCrossCovarianceProduct ε L κp κm π v selectedOrder

Literal paper Step 4(B) identity on the (4.18) cross product.

noncomputable def Anderson4D.SmoothCutoff.r324AllLowDeterministicMomentIntegrand (ρ : SmoothCutoff) (ε L : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The (4.18) integrand with every residual cross covariance projected low. Within-half renormalized factors and all four endpoint phases remain untouched.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324FirstHighDeterministicMomentIntegrand (ρ : SmoothCutoff) (ε L : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The (4.18) integrand whose first high residual cross covariance is the displayed ordered-singles slot.

Equations

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

theorem Anderson4D.SmoothCutoff.deterministicMomentIntegrand_eq_allLow_add_firstHigh (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (x y z w : T4) (v : Fin (2 * m) → T4) : deterministicMomentIntegrand ρ ε m α β κp κm π x y z w v = ρ.r324AllLowDeterministicMomentIntegrand ε L m α β κp κm π x y z w v + ∑ selectedOrder : Fin κp.singles.card, ρ.r324FirstHighDeterministicMomentIntegrand ε L m α β κp κm π selectedOrder x y z w v

Pointwise paper Step 4(B) on the genuine (4.18) integrand. The full signed object is split only into the all-low term and the finite family of first-high operator slots.

The all-low Fourier coefficient vanishes off zero shift

def Anderson4D.SmoothCutoff.r324AllCrossPairModesLow {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) : Prop

Fourier support condition for the all-low cross term.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324AllLowFullPairingFourierIntegral (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) : ℂ

The all-low part of one integrated full-pairing Fourier coefficient. This is the Fourier coefficient obtained after the spatial first-high telescope, before summing configurations.

Equations

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

theorem Anderson4D.SmoothCutoff.not_r324AllCrossPairModesLow_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (q : R324CombinedFourierConfiguration κp κm π) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ¬r324AllCrossPairModesLow ε ‖z4EuclideanFrequency (α + β)‖ κp κm π q

A nonzero integrated Fourier configuration cannot be all-low. This is exactly the capped pigeonhole step used by the paper to delete the all-low term; no pointwise spatial vanishing is asserted.

theorem Anderson4D.SmoothCutoff.r324AllLowFullPairingFourierIntegral_eq_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (q : R324CombinedFourierConfiguration κp κm π) : ρ.r324AllLowFullPairingFourierIntegral ε α β κp κm π q = 0

Consequently every all-low integrated Fourier coefficient is zero at nonzero external shift.

theorem Anderson4D.SmoothCutoff.tsum_r324AllLowFullPairingFourierIntegral_eq_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : ∑' (q : R324CombinedFourierConfiguration κp κm π), ρ.r324AllLowFullPairingFourierIntegral ε α β κp κm π q = 0

The complete all-low Fourier series therefore vanishes, while all configuration and primitive-pairing sums remain signed.

The exact low/high/full guarded configuration

noncomputable def Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedPairModeFactor (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (v : Fin (2 * m) → T4) (r : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) : ℂ

One pair-mode factor in the paper's first-large expansion. Cross slots before the selected slot (in the ordered-singles enumeration) are guarded low, the selected slot is guarded high, and every other pair mode is left full. This remains a fixed Fourier-configuration term; no norm occurs.

Equations

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

theorem Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedPairModeFactor_eq_selectedHigh (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (v : Fin (2 * m) → T4) (r : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) : ρ.r324CanonicalFirstLargeGuardedPairModeFactor ε α β κp κm π hexternal hε hε1 hmtrunc ω v r = ρ.r324SelectedHighPairModeFactor ε ‖z4EuclideanFrequency (α + β)‖ κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) v r

The guards are exact on the canonical nonzero configuration: all earlier modes are genuinely low and the selected mode is genuinely high. Thus the low/high/full factor equals the existing selected-high factor.

noncomputable def Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (v : Fin (2 * m) → T4) : ℂ

Product of the paper-ordered low/high/full factors for one complete Fourier configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedCovarianceConfigurationTerm_eq_selectedHigh (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (v : Fin (2 * m) → T4) : ρ.r324CanonicalFirstLargeGuardedCovarianceConfigurationTerm ε α β κp κm π hexternal hε hε1 hmtrunc ω v = ρ.r324SelectedHighCovarianceConfigurationTerm ε ‖z4EuclideanFrequency (α + β)‖ κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) v

The complete guarded covariance product is exactly the existing selected-high product, without splitting any primitive-pairing sum.

Resumming one fixed selector slot

noncomputable def Anderson4D.SmoothCutoff.r324FixedSelectorGuardedPairModeFactor (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (v : Fin (2 * m) → T4) (r : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) (k : Z4) : ℂ

The unrestricted mode factor for a fixed selector position in the ordered-singles enumeration. This is the literal operator-factor low/high/full decomposition used in paper Step 4(B).

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324FixedSelectorGuardedCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (v : Fin (2 * m) → T4) (q : R324CombinedFourierConfiguration κp κm π) : ℂ

One unrestricted Fourier assignment for the fixed-selector guarded covariance product.

Equations

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

def Anderson4D.SmoothCutoff.r324FixedSelectorConfigurationCondition {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (q : R324CombinedFourierConfiguration κp κm π) : Prop

The configuration-level meaning of the fixed selector: every earlier cross mode is low and the chosen cross mode is high. No condition is put on later cross modes or on within-half pairs.

Equations

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

theorem Anderson4D.SmoothCutoff.r324FixedSelectorConfigurationCondition_iff_firstLargeOrder (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (selectedOrder : Fin κp.singles.card) : r324FixedSelectorConfigurationCondition ε ‖z4EuclideanFrequency (α + β)‖ κp κm π selectedOrder ↑ω ↔ r324FirstLargeResidualIncrementSlot ⋯ (r324EnumeratedCrossSlotIncrement κp κm π ↑ω) hε hε1 ⋯ = selectedOrder

On an endpoint-nonzero configuration, the low-prefix/high-current condition is equivalent to saying that the displayed slot is the canonical first-large slot.

noncomputable def Anderson4D.SmoothCutoff.r324FixedSelectorFilteredCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (v : Fin (2 * m) → T4) (q : R324CombinedFourierConfiguration κp κm π) : ℂ

The original full configuration term restricted to the fixed-selector condition.

Equations

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

theorem Anderson4D.SmoothCutoff.r324FixedSelectorGuardedCovarianceConfigurationTerm_eq_ite (ρ : SmoothCutoff) {m : ℕ} (ε L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (v : Fin (2 * m) → T4) (q : R324CombinedFourierConfiguration κp κm π) : ρ.r324FixedSelectorGuardedCovarianceConfigurationTerm ε L κp κm π selectedOrder v q = ρ.r324FixedSelectorFilteredCovarianceConfigurationTerm ε L κp κm π selectedOrder v q

The factorized low/high/full configuration term is precisely the indicator of the fixed-selector condition times the original full configuration term.

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

The deterministic spatial product after resumming the fixed selector: low covariances before it, the high projected covariance at it, and full covariances at all other pair slots.

Equations

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

theorem Anderson4D.SmoothCutoff.tsum_r324FixedSelectorGuardedCovarianceConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (L : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selectedOrder : Fin κp.singles.card) (v : Fin (2 * m) → T4) : ∑' (q : R324CombinedFourierConfiguration κp κm π), ρ.r324FixedSelectorGuardedCovarianceConfigurationTerm ε L κp κm π selectedOrder v q = ρ.r324FixedSelectorGuardedCovarianceProduct ε L κp κm π selectedOrder v

Exact finite-product Fubini: the unrestricted fixed-selector Fourier series resums to the paper's low/high/full spatial product.

noncomputable def Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedFullPairingFourierIntegrand (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The complete full-pairing Fourier integrand with the paper-order low/high/full guards exposed. All Green factors, endpoint phases, and the complete covariance configuration remain in the same signed term.

Equations

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

theorem Anderson4D.SmoothCutoff.r324CanonicalFirstLargeGuardedFullPairingFourierIntegrand_eq_selectedHigh (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) (x y z w : T4) (v : Fin (2 * m) → T4) : ρ.r324CanonicalFirstLargeGuardedFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω x y z w v = ρ.r324SelectedHighFullPairingFourierIntegrand ε α β κp κm π hexternal hε hε1 hmtrunc ω x y z w v

Exposing all first-large guards leaves the genuine selected-high Fourier integrand unchanged pointwise.

noncomputable def Anderson4D.SmoothCutoff.r324RefinedQuadOpenCovarianceSlotSeries (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) : ℂ

The complete signed open series at one operator position. In particular, the contraction and increment-key components of the route are summed inside this value.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324RefinedQuadSelectedPositionPhysicalIntegrand (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) (q : R324PhysicalPoint m) : ℂ

The genuine five-group physical carrier of one fixed operator slot. The tsum still ranges simultaneously over all contractions and all selector-restricted Fourier configurations in the refined schedule.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RefinedQuadSelectedPositionPhysicalIntegrand_eq_selectedHigh (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) (q : R324PhysicalPoint m) : ρ.r324RefinedQuadSelectedPositionPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p i q = ∑' (a : ρ.R324RefinedQuadSelectedPositionRawFiber hm ε α β hexternal hε hε1 hmtrunc p i), r324Flatten (ρ.r324SelectedHighFullPairingFourierIntegrand ε α β (r324RefinedRawMomentContraction p ↑↑a).fst (r324RefinedRawMomentContraction p ↑↑a).snd.fst (r324RefinedRawMomentContraction p ↑↑a).snd.snd hexternal hε hε1 hmtrunc (ρ.r324RefinedRawNonzeroCombinedConfiguration hm ε α β p ↑↑a ⋯)) q

This fixed-slot physical carrier uses exactly the already-proved canonical selected-high integrands. In particular, no unrestricted projected covariance is substituted for the selector subtype.

theorem Anderson4D.SmoothCutoff.r324RefinedQuadSelectedPositionPhysicalIntegrand_eq_guarded (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) (q : R324PhysicalPoint m) : ρ.r324RefinedQuadSelectedPositionPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p i q = ∑' (a : ρ.R324RefinedQuadSelectedPositionRawFiber hm ε α β hexternal hε hε1 hmtrunc p i), r324Flatten (ρ.r324CanonicalFirstLargeGuardedFullPairingFourierIntegrand ε α β (r324RefinedRawMomentContraction p ↑↑a).fst (r324RefinedRawMomentContraction p ↑↑a).snd.fst (r324RefinedRawMomentContraction p ↑↑a).snd.snd hexternal hε hε1 hmtrunc (ρ.r324RefinedRawNonzeroCombinedConfiguration hm ε α β p ↑↑a ⋯)) q

The same fixed operator-position carrier, now written with the paper's low-before/high-current/full-after guards exposed inside every complete signed Fourier term.

theorem Anderson4D.SmoothCutoff.integral_r324RefinedQuadSelectedPositionPhysicalIntegrand_eq_slotSeries (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (α β : Z4) (hexternal : α + β ≠ 0) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) (i : Fin m) : ∫ (q : R324PhysicalPoint m), ρ.r324RefinedQuadSelectedPositionPhysicalIntegrand hm ε α β hexternal hε hε1 hmtrunc p i q ∂r324PhysicalMeasure m = ρ.r324RefinedQuadOpenCovarianceSlotSeries hm ε α β hexternal hε hε1 hmtrunc p i

Exact Fubini boundary for one operator slot. Absolute summability is inherited from the original raw five-group expansion and is used only to exchange the signed tsum with the physical integral.

theorem Anderson4D.SmoothCutoff.r324RefinedQuadOpenCovarianceSeries_eq_sum_slotSeries (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) : ρ.r324RefinedQuadOpenCovarianceSeries hm ε α β hexternal hε hε1 hmtrunc p = ∑ i : Fin m, ρ.r324RefinedQuadOpenCovarianceSlotSeries hm ε α β hexternal hε hε1 hmtrunc p i

Exact paper-order regrouping: the whole open covariance series is a finite sum over operator positions. No norm occurs in this equality.

theorem Anderson4D.SmoothCutoff.norm_r324RefinedQuadOpenCovarianceSeries_le_sum_slotSeries (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (α β : Z4) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (p : R324RefinedScheduleIndex m) : ‖ρ.r324RefinedQuadOpenCovarianceSeries hm ε α β hexternal hε hε1 hmtrunc p‖ ≤ ∑ i : Fin m, ‖ρ.r324RefinedQuadOpenCovarianceSlotSeries hm ε α β hexternal hε hε1 hmtrunc p i‖

The only triangle inequality introduced by the selector is the finite one over the at most m operator positions. Every primitive-pairing and Fourier sum remains signed inside each summand.

The exact remaining physical consumer boundary

def Anderson4D.SmoothCutoff.R324RefinedQuadOperatorSlotCollapseBound (ρ : SmoothCutoff) (K : ℝ) : Prop

Paper Step 4(B), after the finite choice of an operator factor and before the final Fin m summation. This is a bound on one complete signed slot series: contractions, primitive pairings, routes and Fourier configurations have not been normed separately.

The intended producer first identifies this series with the operator-slot expansion having the chosen factor high-projected, all earlier factors low-projected, and all later factors unprojected. It then repeats the already formalized complete Steps 2--3 collapse on that physical carrier.

Equations

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

theorem Anderson4D.SmoothCutoff.R324RefinedQuadOperatorSlotCollapseBound.toOpenCovarianceSeriesBound {ρ : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : ρ.R324RefinedQuadOperatorSlotCollapseBound K) : ρ.R324RefinedQuadOpenCovarianceSeriesBound (2 * K)

A uniform complete signed bound for one operator slot closes the whole open covariance series. The finite slot count costs only m ≤ 2^m, which is absorbed into the geometric base.