Frequency conservation through the cross-contraction slots

For a doubled moment contraction, the only covariance pairs that can transport Fourier frequency from the left physical copy to the right physical copy are the pairs created from singles of the left partial pairing. This file isolates that statement before any residual-block collapse is performed.

theorem Anderson4D.SmoothCutoff.r324LeftPairModeContribution_momentCombinedPairing_eq_zero_of_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hκp : κp.IsFull) (hκm : κm.IsFull) (q : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card → Z4) (j : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card) : r324LeftPairModeContribution (momentCombinedPairing κp κm π) q j = 0

A within-copy full pairing contributes no mode to translation of the left physical copy.

theorem Anderson4D.SmoothCutoff.r324LeftModeSum_momentCombinedPairing_eq_zero_of_isFull {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hκp : κp.IsFull) (hκm : κm.IsFull) (q : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card → Z4) : r324LeftModeSum (momentCombinedPairing κp κm π) q = 0

If both within-copy partial pairings are full, the complete signed left-mode sum vanishes.

theorem Anderson4D.SmoothCutoff.external_add_eq_zero_of_full_full_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hκp : κp.IsFull) (hκm : κm.IsFull) (q : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card → Z4) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : α + β = 0

A nonzero Fourier configuration built from full pairings in both copies can occur only at zero external shift.

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

A nonzero configuration at nonzero external shift must contain a cross-copy contraction slot.

theorem Anderson4D.SmoothCutoff.r324FullPairingFourierIntegral_eq_zero_of_singles_empty (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hsingles : κp.singles = ∅) (q : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card → Z4) : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q = 0

At nonzero external shift, a configuration with no left cross slot vanishes identically. This is the form used to discard the full/full branch before selecting a marked covariance slot.

theorem Anderson4D.SmoothCutoff.r324FullPairingFourierIntegral_eq_zero_of_left_isFull (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (hexternal : α + β ≠ 0) (hκp : κp.IsFull) (q : Fin {i ∈ (momentCombinedPairing κp κm π).pairSupport | i < (momentCombinedPairing κp κm π) i}.card → Z4) : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q = 0

Equivalent vanishing statement when fullness of the left partial pairing is the available hypothesis.

noncomputable def Anderson4D.SmoothCutoff.r324CrossSlotPairIndex {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (i : ↥κp.singles) : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card

The enumerated pair index of the cross-copy pair generated by one single of the left partial pairing. This enumerates exactly κp.singles; within-copy covariance pairs are absent.

Equations

• Anderson4D.SmoothCutoff.r324CrossSlotPairIndex κp κm π i = (Anderson4D.SmoothCutoff.r324PairFinEquiv (Anderson4D.momentCombinedPairing κp κm π)).symm ⟨Anderson4D.leftMomentIndex ↑i, ⋯⟩

@[simp]

theorem Anderson4D.SmoothCutoff.r324PairFinEquiv_r324CrossSlotPairIndex {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (i : ↥κp.singles) : ↑((r324PairFinEquiv (momentCombinedPairing κp κm π)) (r324CrossSlotPairIndex κp κm π i)) = leftMomentIndex ↑i

theorem Anderson4D.SmoothCutoff.r324CrossSlotPairIndex_injective {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Function.Injective (r324CrossSlotPairIndex κp κm π)

@[simp]

theorem Anderson4D.SmoothCutoff.r324LeftPairModeContribution_r324CrossSlotPairIndex {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (i : ↥κp.singles) : r324LeftPairModeContribution (momentCombinedPairing κp κm π) q (r324CrossSlotPairIndex κp κm π i) = q (r324CrossSlotPairIndex κp κm π i)

At a cross slot, the signed left-copy contribution is the assigned pair mode with positive sign.

theorem Anderson4D.SmoothCutoff.r324LeftPairModeContribution_eq_zero_of_not_crossSlot {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (j : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card) (hj : ∀ (i : ↥κp.singles), r324CrossSlotPairIndex κp κm π i ≠ j) : r324LeftPairModeContribution (momentCombinedPairing κp κm π) q j = 0

Every enumerated pair outside the image of the cross-slot enumeration contributes zero to left-copy translation.

noncomputable def Anderson4D.SmoothCutoff.r324CrossSlotLatticeIncrement {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (i : ↥κp.singles) : Z4

The lattice-frequency increment attached to one cross-contraction slot, with the sign chosen so that the total is the external shift.

Equations

• Anderson4D.SmoothCutoff.r324CrossSlotLatticeIncrement κp κm π q i = -q (Anderson4D.SmoothCutoff.r324CrossSlotPairIndex κp κm π i)

noncomputable def Anderson4D.SmoothCutoff.r324CrossSlotIncrement {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (i : ↥κp.singles) : EuclideanSpace ℝ (Fin dim)

Euclidean realization of a cross-contraction-slot increment.

Equations

• Anderson4D.SmoothCutoff.r324CrossSlotIncrement κp κm π q i = Anderson4D.z4EuclideanFrequency (Anderson4D.SmoothCutoff.r324CrossSlotLatticeIncrement κp κm π q i)

theorem Anderson4D.SmoothCutoff.sum_r324CrossSlotLatticeIncrement {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) : ∑ i : ↥κp.singles, r324CrossSlotLatticeIncrement κp κm π q i = -r324LeftModeSum (momentCombinedPairing κp κm π) q

Cross slots alone carry the entire negative signed left-mode sum. All within-copy covariance pairs cancel before this equality is used.

theorem Anderson4D.SmoothCutoff.sum_r324CrossSlotLatticeIncrement_eq_external_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ∑ i : ↥κp.singles, r324CrossSlotLatticeIncrement κp κm π q i = α + β

Under the existing nonzero-integral conservation law, the cross-contraction-slot lattice increments sum to the exact external Fourier shift.

theorem Anderson4D.SmoothCutoff.sum_r324CrossSlotIncrement_eq_external_of_integral_ne_zero (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (q : Fin {a ∈ (momentCombinedPairing κp κm π).pairSupport | a < (momentCombinedPairing κp κm π) a}.card → Z4) (hne : ρ.r324FullPairingFourierIntegral ε α β ⟨momentCombinedPairing κp κm π, ⋯⟩ q ≠ 0) : ∑ i : ↥κp.singles, r324CrossSlotIncrement κp κm π q i = z4EuclideanFrequency (α + β)

Euclidean cross-slot increments likewise sum to the exact external frequency vector.