Finite type counts, hierarchy separation and tensor execution bounds.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} [DecidableEq S] [DecidableEq U] (lx : X → S) (T : Tensor ℂ X Y Z) : Tensor ℂ (X × U) (Y × U) (Z × S)

Retain tensor entries with matching branch labels and a shared auxiliary coordinate.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.separatedTensor lx T x y z = if lx x.1 = z.2 ∧ x.2 = y.2 then T x.1 y.1 z.1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_separation_identity {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} {G : Type u_6} [AddCommGroup G] [DecidableEq G] [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (tag : S → G) (point : S → U → G) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hcollision : ∀ (s s' : S) (i j : U), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j) : Tensor.pullback (fun (x : X × U) => (x.1, point (lx x.1) x.2)) (fun (y : Y × U) => (y.1, tag (ly y.1) - point (ly y.1) y.2)) (fun (z : Z × S) => (z.1, tag z.2)) (T.product (groupTensor G)) = separatedTensor lx T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_separation_mem_restrictionOrbit {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} {G : Type u_6} [AddCommGroup G] [Fintype G] [DecidableEq G] [DecidableEq S] [DecidableEq U] [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (tag : S → G) (point : S → U → G) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hcollision : ∀ (s s' : S) (i j : U), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j) : separatedTensor lx T ∈ (T.product (groupTensor G)).restrictionOrbit

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_separation_degeneratesTo {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} {G : Type u_6} [AddCommGroup G] [Fintype G] [DecidableEq G] [DecidableEq S] [DecidableEq U] [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (tag : S → G) (point : S → U → G) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hcollision : ∀ (s s' : S) (i j : U), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j) : (T.product (groupTensor G)).DegeneratesTo (separatedTensor lx T)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_separation_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} {G : Type u_6} [AddCommGroup G] [Fintype G] [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (tag : S → G) (point : S → U → G) {r : ℕ} (hT : T.RankAtMost r) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hcollision : ∀ (s s' : S) (i j : U), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j) : (separatedTensor lx T).RankAtMost (r * Fintype.card G)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_separation_borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} {U : Type u_5} {G : Type u_6} [AddCommGroup G] [Fintype G] [DecidableEq S] [DecidableEq U] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) (tag : S → G) (point : S → U → G) {r : ℕ} (hT : T.BorderRankAtMost r) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) (hcollision : ∀ (s s' : S) (i j : U), point s i + (tag s - point s j) = tag s' ↔ s = s' ∧ i = j) : (separatedTensor lx T).BorderRankAtMost (r * Fintype.card G)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_grid_separation_mem_restrictionOrbit {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} [Fintype S] [DecidableEq S] [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {d Q m : ℕ} [NeZero (4 * Q)] (hK : (d * Q ^ 2 + 1) * Fintype.card S ≤ Q ^ d) (hm : (d * Q ^ 2 + 1) * m ≤ Q ^ d) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : separatedTensor lx T ∈ (T.product (groupTensor (Separation.AuxiliaryGroup d Q))).restrictionOrbit

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_grid_separation_rankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} [Fintype S] [DecidableEq S] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {d Q m r : ℕ} (hQ : 0 < Q) (hK : (d * Q ^ 2 + 1) * Fintype.card S ≤ Q ^ d) (hm : (d * Q ^ 2 + 1) * m ≤ Q ^ d) (hT : T.RankAtMost r) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : (separatedTensor lx T).RankAtMost (r * (4 * Q) ^ d)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.finite_grid_separation_borderRankAtMost {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {S : Type u_4} [Fintype S] [DecidableEq S] (T : Tensor ℂ X Y Z) (lx : X → S) (ly : Y → S) {d Q m r : ℕ} (hQ : 0 < Q) (hK : (d * Q ^ 2 + 1) * Fintype.card S ≤ Q ^ d) (hm : (d * Q ^ 2 + 1) * m ≤ Q ^ d) (hT : T.BorderRankAtMost r) (hlabels : ∀ (x : X) (y : Y) (z : Z), T x y z ≠ 0 → lx x = ly y) : (separatedTensor lx T).BorderRankAtMost (r * (4 * Q) ^ d)