Selecting the high-frequency cross-contraction slot

This file connects the exact cross-slot conservation law for one actual Fourier configuration to the first-large-increment selector. The selected left single is then mapped back to the genuine pair index of the doubled pairing and to the existing one-projected-covariance construction.

The scope remains the Fourier-configuration layer. In particular, no declaration below identifies the original R-324 moment with a projected configuration series, and no residual-block collapse is performed.

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324CombinedFourierConfiguration {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

Fourier assignments for the actual full doubled pairing attached to one contraction triple.

Equations

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

@[reducible, inline]

abbrev Anderson4D.SmoothCutoff.R324NonzeroCombinedFourierConfiguration (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Type

The actual Fourier configurations whose physical integral is nonzero. This is only a subtype of configurations, not a decomposition of the original moment.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324EnumeratedCrossSlotIncrement {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (j : Fin κp.singles.card) : EuclideanSpace ℝ (Fin dim)

Cross-slot increments enumerated by the standard Fin card enumeration required by the first-large selector.

Equations

• Anderson4D.SmoothCutoff.r324EnumeratedCrossSlotIncrement κp κm π q j = Anderson4D.SmoothCutoff.r324CrossSlotIncrement κp κm π q ((Anderson4D.r324ResidualCovarianceSlotEquiv κp) j)

theorem Anderson4D.SmoothCutoff.sum_r324EnumeratedCrossSlotIncrement_eq_external_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ∑ j : Fin κp.singles.card, r324EnumeratedCrossSlotIncrement κp κm π q j = z4EuclideanFrequency (α + β)

Reindexing by Fin κp.singles.card preserves the exact cross-slot frequency sum.

theorem Anderson4D.SmoothCutoff.r324CrossSlot_card_pos_of_external_ne_zero_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (q : R324CombinedFourierConfiguration κp κm π) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : 0 < κp.singles.card

At nonzero external shift, an actual nonzero configuration has a positive number of cross slots.

theorem Anderson4D.SmoothCutoff.exists_r324CrossSlotIncrement_average (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (q : R324CombinedFourierConfiguration κp κm π) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ∃ (i : R324ResidualCovarianceSlot κp), ‖z4EuclideanFrequency (α + β)‖ ≤ ↑κp.singles.card * ‖r324CrossSlotIncrement κp κm π q i‖

Average-size routing in the literal division-free form: one genuine cross slot carries at least 1 / card of the external shift.

theorem Anderson4D.SmoothCutoff.exists_r324CrossSlotIncrement_norm_div_card_le (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (q : R324CombinedFourierConfiguration κp κm π) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ∃ (i : R324ResidualCovarianceSlot κp), ‖z4EuclideanFrequency (α + β)‖ / ↑κp.singles.card ≤ ‖r324CrossSlotIncrement κp κm π q i‖

The same average-size conclusion in the explicit quotient form.

theorem Anderson4D.SmoothCutoff.r324CrossSlot_card_le_truncOrder {m : ℕ} {ε : ℝ} (κp : PartialPairing (Fin m)) (hmtrunc : m ≤ truncOrder ε) : κp.singles.card ≤ truncOrder ε

The number of cross slots is within the truncation order whenever the moment order is.

noncomputable def Anderson4D.SmoothCutoff.r324FirstLargeCrossSlot {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : R324ResidualCovarianceSlot κp

The canonical first cross slot meeting the paper's sqrt ε / 2 routing threshold. The positivity proof is explicit so the definition itself does not pretend that every pairing has a cross slot.

Equations

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

noncomputable def Anderson4D.SmoothCutoff.r324FirstLargeCrossPairIndex {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card

The selected residual slot mapped to the actual pair index in the combined full pairing.

Equations

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

theorem Anderson4D.SmoothCutoff.r324PairFinEquiv_r324FirstLargeCrossPairIndex {m : ℕ} (ε : ℝ) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) : ↑((r324PairFinEquiv (momentCombinedPairing κp κm π)) (r324FirstLargeCrossPairIndex ε κp κm π q hcard hε hε1 hmtrunc)) = leftMomentIndex ↑(r324FirstLargeCrossSlot ε κp κm π q hcard hε hε1 hmtrunc)

The mapped selected pair index has precisely the left-single lower endpoint in the actual combined pairing.

theorem Anderson4D.SmoothCutoff.r324FirstLargeCrossSlot_spec_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : √ε / 2 * ‖z4EuclideanFrequency (α + β)‖ ≤ ‖r324CrossSlotIncrement κp κm π q (r324FirstLargeCrossSlot ε κp κm π q hcard hε hε1 hmtrunc)‖

For a nonzero actual configuration, the canonical selected cross slot satisfies the exact truncation-scale threshold.

theorem Anderson4D.SmoothCutoff.r324FirstLargeCrossSlot_spec_of_external_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (q : R324CombinedFourierConfiguration κp κm π) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : have hcard := ⋯; √ε / 2 * ‖z4EuclideanFrequency (α + β)‖ ≤ ‖r324CrossSlotIncrement κp κm π q (r324FirstLargeCrossSlot ε κp κm π q hcard hε hε1 hmtrunc)‖

At nonzero external shift the positivity premise of the canonical selector is supplied by the actual configuration itself.

theorem Anderson4D.SmoothCutoff.norm_r324CrossSlotIncrement_eq_pairMode {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (i : R324ResidualCovarianceSlot κp) : ‖r324CrossSlotIncrement κp κm π q i‖ = ‖z4EuclideanFrequency (q (r324CrossSlotPairIndex κp κm π i))‖

The norm of a cross-slot increment is exactly the norm of the Fourier mode assigned to its genuine combined-pair index.

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

The actual mode on the selected combined-pair index belongs to the high-mode set used by r324ProjectedCovarianceC.

theorem Anderson4D.SmoothCutoff.r324HighCovarianceModeTerm_firstLargeCrossPairMode (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) (z : T4) : ρ.r324HighCovarianceModeTerm ε ‖z4EuclideanFrequency (α + β)‖ z (q (r324FirstLargeCrossPairIndex ε κp κm π q hcard hε hε1 hmtrunc)) = ρ.r324CovarianceModeTerm ε z (q (r324FirstLargeCrossPairIndex ε κp κm π q hcard hε hε1 hmtrunc))

Consequently the selected actual Fourier mode is retained, unchanged, by the high-covariance mode indicator.

noncomputable def Anderson4D.SmoothCutoff.r324FirstLargeSingleProjectedResidualCovarianceProduct (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (v : Fin (2 * m) → T4) : ℂ

The concrete residual covariance product obtained by projecting exactly the canonical selected cross slot.

Equations

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

theorem Anderson4D.SmoothCutoff.r324FirstLargeSingleProjectedResidualCovarianceProduct_eq (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : R324CombinedFourierConfiguration κp κm π) (hcard : 0 < κp.singles.card) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (v : Fin (2 * m) → T4) : ρ.r324FirstLargeSingleProjectedResidualCovarianceProduct ε α β κp κm π q hcard hε hε1 hmtrunc v = ρ.r324ProjectedCovarianceC ε ‖z4EuclideanFrequency (α + β)‖ (r324ResidualCovarianceDisplacement κp κm π v (r324FirstLargeCrossSlot ε κp κm π q hcard hε hε1 hmtrunc)) * ∏ i ∈ Finset.univ.erase (r324FirstLargeCrossSlot ε κp κm π q hcard hε hε1 hmtrunc), ↑(ρ.etaEpsT4 ε (r324ResidualCovarianceDisplacement κp κm π v i))

Exact factorization of the selected product: one projected covariance and complete etaEpsT4 factors at every other cross slot.

noncomputable def Anderson4D.SmoothCutoff.r324FirstLargeCrossSlotForNonzeroConfiguration (ρ : 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 π) : R324ResidualCovarianceSlot κp

Canonical selected slot as a function of an actual nonzero Fourier configuration. Nonzero external shift supplies the required nonempty cross-slot proof for every member of the subtype.

Equations

• ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω = Anderson4D.SmoothCutoff.r324FirstLargeCrossSlot ε κp κm π ↑ω ⋯ hε hε1 hmtrunc

theorem Anderson4D.SmoothCutoff.r324FirstLargeCrossSlotForNonzeroConfiguration_spec (ρ : 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 π) : √ε / 2 * ‖z4EuclideanFrequency (α + β)‖ ≤ ‖r324CrossSlotIncrement κp κm π (↑ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)‖

Every nonzero actual configuration is covered by its canonical selected cross slot at the paper's high-mode threshold.

noncomputable def Anderson4D.SmoothCutoff.r324FirstLargeCrossPairIndexForNonzeroConfiguration (ρ : 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 π) : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card

The canonical selected slot of a nonzero configuration, mapped to its genuine pair index in the combined full pairing.

Equations

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

theorem Anderson4D.SmoothCutoff.r324PairFinEquiv_firstLargeCrossPairIndexForNonzeroConfiguration (ρ : 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 π) : ↑((r324PairFinEquiv (momentCombinedPairing κp κm π)) (ρ.r324FirstLargeCrossPairIndexForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)) = leftMomentIndex ↑(ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)

The actual selected pair index has the expected left-single lower endpoint.

theorem Anderson4D.SmoothCutoff.firstLargeCrossPairModeForNonzeroConfiguration_mem_highModeSet (ρ : 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 π) : ↑ω (ρ.r324FirstLargeCrossPairIndexForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω) ∈ r324HighModeSet ε ‖z4EuclideanFrequency (α + β)‖

The actual Fourier mode carried by the selected genuine pair index is retained by the one-slot high-frequency projection.

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

A concrete family over actual nonzero configurations in which the canonical cross slot is projected and every other cross covariance is left complete. The amplitude and physical variables remain explicit: no equality with the original moment is asserted.

Equations

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

theorem Anderson4D.SmoothCutoff.r324ActualCrossRoutedSingleProjectedTerm_eq (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (v : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π → Fin (2 * m) → T4) (amplitude : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π → ℂ) (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π) : ρ.r324ActualCrossRoutedSingleProjectedTerm ε α β κp κm π hexternal hε hε1 hmtrunc v amplitude ω = amplitude ω * (ρ.r324ProjectedCovarianceC ε ‖z4EuclideanFrequency (α + β)‖ (r324ResidualCovarianceDisplacement κp κm π (v ω) (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω)) * ∏ i ∈ Finset.univ.erase (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc ω), ↑(ρ.etaEpsT4 ε (r324ResidualCovarianceDisplacement κp κm π (v ω) i)))

Pointwise structure of the routed term: exactly one projected covariance, multiplied by complete etaEpsT4 factors at all remaining cross slots.

theorem Anderson4D.SmoothCutoff.norm_tsum_r324ActualCrossRoutedSingleProjectedTerm_le (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hε : 0 < ε) (hε1 : ε ≤ 1) (hmtrunc : m ≤ truncOrder ε) (v : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π → Fin (2 * m) → T4) (amplitude : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π → ℂ) (hterm : Summable (ρ.r324ActualCrossRoutedSingleProjectedTerm ε α β κp κm π hexternal hε hε1 hmtrunc v amplitude)) : ‖∑' (ω : ρ.R324NonzeroCombinedFourierConfiguration ε α β κp κm π), ρ.r324ActualCrossRoutedSingleProjectedTerm ε α β κp κm π hexternal hε hε1 hmtrunc v amplitude ω‖ ≤ ∑ i : R324ResidualCovarianceSlot κp, r324SingleProjectedSlotMass (ρ.r324FirstLargeCrossSlotForNonzeroConfiguration ε α β κp κm π hexternal hε hε1 hmtrunc) (ρ.r324ActualCrossRoutedSingleProjectedTerm ε α β κp κm π hexternal hε hε1 hmtrunc v amplitude) i

Finite slot-fibre bound for the actual nonzero-configuration family. The selected-slot function is canonical, so the fibres are disjoint; the finite index type has at most m elements.