SquareWeights.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

+# The square weights in auxiliary separation

Sections 4.1–4.3 use the phase u - v + 2 * (g - h) to select monomials. On a selected monomial, the three integer variable weights add to (g - h)^2. Thus the surviving monomials have nonnegative total degree, although individual variable weights may be negative. Their degree is zero precisely when the guess g matches the sector h and the auxiliary labels agree.

def OAI.MatrixMultiplication.AuxiliarySeparation.phase line 18
Source documentation
The exponent occurring in the finite Fourier projection.
```
def phase (g h u v : ℤ) : ℤ := u - v + 2 * (g - h)
```
def OAI.MatrixMultiplication.AuxiliarySeparation.firstWeight line 21
Source documentation
Weight on the first tensor leg, which carries the guessed sector label.
```
def firstWeight (g : ℤ) : ℤ := g ^ 2
```
def OAI.MatrixMultiplication.AuxiliarySeparation.secondWeight line 24
Source documentation
Weight on the second tensor leg.
```
def secondWeight (h u : ℤ) : ℤ := h * u - h ^ 2
```
def OAI.MatrixMultiplication.AuxiliarySeparation.thirdWeight line 27
Source documentation
Weight on the third tensor leg.
```
def thirdWeight (h v : ℤ) : ℤ := -(h * v)
```
def OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight line 30
Source documentation
Total weight of a target monomial after the three independent substitutions.
```
def totalWeight (g h u v : ℤ) : ℤ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_eq_square_add_phase line 33
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_eq_sq_of_phase_eq_zero line 39
Source documentation
The projection equation converts the total weight into a square.
```
theorem totalWeight_eq_sq_of_phase_eq_zero {g h u v : ℤ}
    (hphase : phase g h u v = 0) :
    totalWeight g h u v = (g - h) ^ 2 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.phase, OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_nonneg_of_phase_eq_zero line 44
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_eq_zero_iff_of_phase_eq_zero line 50
Source documentation
On the Fourier support, precisely the correctly matched terms have weight zero.
```
theorem totalWeight_eq_zero_iff_of_phase_eq_zero {g h u v : ℤ}
    (hphase : phase g h u v = 0) :
    totalWeight g h u v = 0 ↔ g = h ∧ u = v := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.phase, OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight
theorem OAI.MatrixMultiplication.AuxiliarySeparation.phase_and_totalWeight_eq_zero_iff line 63
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_pos_iff_of_phase_eq_zero line 71
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight_le_of_labels line 77
Source documentation
The degree bound in Section 4.3, for sector labels in 1, …, M.
```
theorem totalWeight_le_of_labels {M g h u v : ℤ}
    (hg : 1 ≤ g ∧ g ≤ M) (hh : 1 ≤ h ∧ h ≤ M)
    (hphase : phase g h u v = 0) :
    totalWeight g h u v ≤ (M - 1) ^ 2 := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.phase, OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight
def OAI.MatrixMultiplication.AuxiliarySeparation.totalDegree line 87
Source documentation
The polynomial degree attached to a surviving monomial.
```
def totalDegree (g h u v : ℤ) : ℕ := (totalWeight g h u v).toNat
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.totalWeight
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalDegree_cast_of_phase_eq_zero line 89
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalDegree_eq_zero_iff_of_phase_eq_zero line 94
theorem OAI.MatrixMultiplication.AuxiliarySeparation.totalDegree_le_of_labels line 101