NoWrap.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

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 OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le line 19

Source documentation

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

theorem 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) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierRadius_lt_modulus line 27
Source documentation
The Fourier modulus exceeds the full possible range of the exponent.
```
theorem fourierRadius_lt_modulus {M : ℤ} (hM : 1 ≤ M) :
    3 * (M - 1) < 5 * M := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_lt line 32

Source documentation

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

theorem 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 :=
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_eq_zero_of_dvd line 39

Source documentation

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

theorem 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 :=
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero line 47

Source documentation

Characterization of the surviving Fourier support without modular arithmetic.

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le_nat line 58

Source documentation

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

theorem 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) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero_nat line 65

Source documentation

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

theorem 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 := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_abs_le_fin line 73
Source documentation
Zero-based finite labels have the same exponent as the paper's labels plus one.
```
theorem fourierPhase_abs_le_fin {M : ℕ} (h g u v : Fin M) :
    |(u.val : ℤ) - v.val + 2 * ((g.val : ℤ) - h.val)| ≤
      3 * ((M : ℤ) - 1) := by
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.fourierPhase_dvd_iff_eq_zero_fin line 84

Source documentation

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

theorem fourierPhase_dvd_iff_eq_zero_fin {M : ℕ} (h g u v : Fin M) :
    ((5 : ℤ) * M ∣ (u.val : ℤ) - v.val + 2 * ((g.val : ℤ) - h.val)) ↔
      (u.val : ℤ) - v.val + 2 * ((g.val : ℤ) - h.val) = 0 := by
…