+# 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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.phase (g h u v : ℤ) : ℤ

The exponent occurring in the finite Fourier projection.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.phase g h u v = u - v + 2 * (g - h)

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.firstWeight (g : ℤ) : ℤ

Weight on the first tensor leg, which carries the guessed sector label.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.firstWeight g = g ^ 2

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.secondWeight (h u : ℤ) : ℤ

Weight on the second tensor leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.secondWeight h u = h * u - h ^ 2

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.thirdWeight (h v : ℤ) : ℤ

Weight on the third tensor leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.thirdWeight h v = -(h * v)

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalWeight (g h u v : ℤ) : ℤ

Total weight of a target monomial after the three independent substitutions.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalWeight_eq_square_add_phase (g h u v : ℤ) : totalWeight g h u v = (g - h) ^ 2 + h * phase g h u v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

The projection equation converts the total weight into a square.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalWeight_nonneg_of_phase_eq_zero {g h u v : ℤ} (hphase : phase g h u v = 0) : 0 ≤ totalWeight g h u v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

On the Fourier support, precisely the correctly matched terms have weight zero.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.phase_and_totalWeight_eq_zero_iff (g h u v : ℤ) : phase g h u v = 0 ∧ totalWeight g h u v = 0 ↔ g = h ∧ u = v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalWeight_pos_iff_of_phase_eq_zero {g h u v : ℤ} (hphase : phase g h u v = 0) : 0 < totalWeight g h u v ↔ g ≠ h

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.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

The degree bound in Section 4.3, for sector labels in 1, …, M.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalDegree (g h u v : ℤ) : ℕ

The polynomial degree attached to a surviving monomial.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalDegree g h u v = (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalWeight g h u v).toNat

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalDegree_cast_of_phase_eq_zero {g h u v : ℤ} (hphase : phase g h u v = 0) : ↑(totalDegree g h u v) = totalWeight g h u v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalDegree_eq_zero_iff_of_phase_eq_zero {g h u v : ℤ} (hphase : phase g h u v = 0) : totalDegree g h u v = 0 ↔ g = h ∧ u = v

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.totalDegree_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) : totalDegree g h u v ≤ (M - 1) ^ 2