Finite type counts, hierarchy separation and tensor execution bounds.

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.AuxiliaryGroup (d Q : ℕ) : Type

Finite product of cyclic groups containing the integer separation grid.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.AuxiliaryGroup d Q = (Fin d → ZMod (4 * Q))

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridToGroup {d Q : ℕ} (x : Grid d Q) : AuxiliaryGroup d Q

Embed an integer grid point into the finite ambient separation group.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridToGroup x i = ↑↑(x i)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridToReal {d Q : ℕ} (x : Grid d Q) : Fin d → ℝ

Embed an integer grid point into real coordinate space.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridToReal x i = ↑↑(x i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.gridToReal_injective {d Q : ℕ} : Function.Injective gridToReal

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm_gridToReal {d Q : ℕ} (x : Grid d Q) : squaredNorm (gridToReal x) = ↑(gridSquaredNorm x)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.dot_gridToReal {d Q : ℕ} (x y : Grid d Q) : dot (gridToReal x) (gridToReal y) = ↑(gridDot x y)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.grid_group_collision_lift {d Q : ℕ} (t c u v : Grid d Q) (h : gridToGroup u + (gridToGroup t - gridToGroup v) = gridToGroup c) (i : Fin d) : ↑↑(c i) = ↑↑(t i) + ↑↑(u i) - ↑↑(v i)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.grid_sphere_slice_collision {d Q : ℕ} (t c u v : Grid d Q) (hsphere : gridSquaredNorm c = gridSquaredNorm t) (hslice : gridDot t u = gridDot t v) : gridToGroup u + (gridToGroup t - gridToGroup v) = gridToGroup c ↔ u = v ∧ c = t

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.indexed_grid_collision {S : Type u_1} {U : Type u_2} {d Q : ℕ} (tag : S → Grid d Q) (point : S → U → Grid d Q) (htag : Function.Injective tag) (hpoint : ∀ (s : S), Function.Injective (point s)) (hsphere : ∀ (s s' : S), gridSquaredNorm (tag s') = gridSquaredNorm (tag s)) (hslice : ∀ (s : S) (i j : U), gridDot (tag s) (point s i) = gridDot (tag s) (point s j)) (s s' : S) (i j : U) : gridToGroup (point s i) + (gridToGroup (tag s) - gridToGroup (point s j)) = gridToGroup (tag s') ↔ s = s' ∧ i = j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.exists_modular_separation {d Q K m : ℕ} (hK : (d * Q ^ 2 + 1) * K ≤ Q ^ d) (hm : (d * Q ^ 2 + 1) * m ≤ Q ^ d) : ∃ (tag : Fin K → AuxiliaryGroup d Q) (point : Fin K → Fin m → AuxiliaryGroup d Q), ∀ (s s' : Fin K) (i j : Fin m), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Separation.card_auxiliaryGroup (d Q : ℕ) [NeZero (4 * Q)] : Fintype.card (AuxiliaryGroup d Q) = (4 * Q) ^ d