The Fourier projection has no modular wrap

Section 4.1 of Matrix Multiplication via Auxiliary Separation and Polynomial Multiplication uses exactly 5 * M Fourier phases. The exponent u - v + 2 * (g - h) has absolute value at most 3 * (M - 1) when all four labels lie in {1, ..., M}. Consequently, divisibility by 5 * M is equivalent to the exact integer support equation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le {M h g u v : ℤ} (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : |u - v + 2 * (g - h)| ≤ 3 * (M - 1)

The explicit bound for the exponent in the finite Fourier projection.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierRadius_lt_modulus {M : ℤ} (hM : 1 ≤ M) : 3 * (M - 1) < 5 * M

The Fourier modulus exceeds the full possible range of the exponent.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_lt {M h g u v : ℤ} (hM : 1 ≤ M) (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : |u - v + 2 * (g - h)| < 5 * M

Every possible exponent lies strictly between minus and plus the modulus.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_eq_zero_of_dvd {M h g u v : ℤ} (hM : 1 ≤ M) (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) (hdiv : 5 * M ∣ u - v + 2 * (g - h)) : u - v + 2 * (g - h) = 0

Modular Fourier support is exact integer support for the allowed labels.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero {M h g u v : ℤ} (hM : 1 ≤ M) (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : 5 * M ∣ u - v + 2 * (g - h) ↔ u - v + 2 * (g - h) = 0

Characterization of the surviving Fourier support without modular arithmetic.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero_of_lt {M L h g u v : ℤ} (hL : 3 * (M - 1) < L) (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : L ∣ u - v + 2 * (g - h) ↔ u - v + 2 * (g - h) = 0

Characterization of the surviving Fourier support for an arbitrary period L > 3 * (M - 1) (all-fields version: the period need not be 5 * M).

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le_nat {M h g u v : ℕ} (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : |↑u - ↑v + 2 * (↑g - ↑h)| ≤ 3 * (↑M - 1)

The same exponent bound for natural-number labels, interpreted in ℤ.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero_nat {M h g u v : ℕ} (hM : 1 ≤ M) (hh : 1 ≤ h ∧ h ≤ M) (hg : 1 ≤ g ∧ g ≤ M) (hu : 1 ≤ u ∧ u ≤ M) (hv : 1 ≤ v ∧ v ≤ M) : 5 * ↑M ∣ ↑u - ↑v + 2 * (↑g - ↑h) ↔ ↑u - ↑v + 2 * (↑g - ↑h) = 0

Natural-number labels admit no additional solutions modulo 5 * M.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le_fin {M : ℕ} (h g u v : Fin M) : |↑↑u - ↑↑v + 2 * (↑↑g - ↑↑h)| ≤ 3 * (↑M - 1)

Zero-based finite labels have the same exponent as the paper's labels plus one.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero_fin {M : ℕ} (h g u v : Fin M) : 5 * ↑M ∣ ↑↑u - ↑↑v + 2 * (↑↑g - ↑↑h) ↔ ↑↑u - ↑↑v + 2 * (↑↑g - ↑↑h) = 0

The support test for a Fourier projection indexed by Fin M.