Coordinate identifications of the three retained sectors

Each outer branch is a zero extension of C(a,h), using the same first-leg coordinates. The middle branch is a zero extension after reversing the first coordinate and exchanging the second and third tensor legs.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftY (a h : ℕ) (r : Fin h) : YIndex a h

Embed the left second-leg interval.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftY a h r = ⟨↑r, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ (a h : ℕ) (s : Fin (a + h - 1)) : ZIndex a h

Embed the left third-leg interval.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ a h s = ⟨↑s, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleY (a h : ℕ) (s : Fin (a + h - 1)) : YIndex a h

Embed the middle second-leg interval, which carries the convolution output.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleY a h s = ⟨h + ↑s, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ (a h : ℕ) (r : Fin h) : ZIndex a h

Embed the middle third-leg interval, which carries the second input.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ a h r = ⟨h + a - 1 + ↑r, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightY (a h : ℕ) (r : Fin h) : YIndex a h

Embed the right second-leg interval.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightY a h r = ⟨MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart a h + ↑r, ⋯⟩

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ (a h : ℕ) (s : Fin (a + h - 1)) : ZIndex a h

Embed the right third-leg interval.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ a h s = ⟨MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart a h + ↑s, ⋯⟩

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftY_injective (a h : ℕ) : Function.Injective (leftY a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftZ_injective (a h : ℕ) : Function.Injective (leftZ a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleY_injective (a h : ℕ) : Function.Injective (middleY a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleZ_injective (a h : ℕ) : Function.Injective (middleZ a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightY_injective (a h : ℕ) : Function.Injective (rightY a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightZ_injective (a h : ℕ) : Function.Injective (rightZ a h)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_pullback {K : Type} [Field K] (a h : ℕ) : Foundation.Tensor.pullback id (leftY a h) (leftZ a h) (leftTensor K a h) = convolution K a h

Pulling back the left block gives ordinary convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_pullback {K : Type} [Field K] (a h : ℕ) : Foundation.Tensor.pullback id (rightY a h) (rightZ a h) (rightTensor K a h) = convolution K a h

Pulling back the translated right block also gives ordinary convolution.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (Fin (a + h - 1)) (Fin h)

Exchange the two outer convolution legs while retaining the original input order in the displayed coefficient equation.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_pullback {K : Type} [Field K] (a h : ℕ) : Foundation.Tensor.pullback Fin.rev (middleY a h) (middleZ a h) (middleTensor K a h) = exchangedConvolution K a h

The middle branch is exactly convolution with its last two legs exchanged; the first-leg reversal occurs solely in this individual branch identification.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_support {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) (hn : leftTensor K a h i j k ≠ 0) : (∃ (r : Fin h), leftY a h r = j) ∧ ∃ (s : Fin (a + h - 1)), leftZ a h s = k

All nonzero left-branch coordinates lie in the displayed embeddings.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_support {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) (hn : rightTensor K a h i j k ≠ 0) : (∃ (r : Fin h), rightY a h r = j) ∧ ∃ (s : Fin (a + h - 1)), rightZ a h s = k

All nonzero right-branch coordinates lie in the translated embeddings.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_support {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) (hn : middleTensor K a h i j k ≠ 0) : (∃ (u : Fin a), u.rev = i) ∧ (∃ (s : Fin (a + h - 1)), middleY a h s = j) ∧ ∃ (r : Fin h), middleZ a h r = k

All nonzero middle-branch coordinates lie in the exchanged embeddings.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_eq_extension {K : Type} [Field K] (a h : ℕ) : leftTensor K a h = Foundation.Tensor.restrict (fun (x i : Fin a) => if i = x then 1 else 0) (fun (y : YIndex a h) (r : Fin h) => if leftY a h r = y then 1 else 0) (fun (z : ZIndex a h) (s : Fin (a + h - 1)) => if leftZ a h s = z then 1 else 0) (convolution K a h)

The left block is the zero extension of the ordinary convolution tensor.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_eq_extension {K : Type} [Field K] (a h : ℕ) : rightTensor K a h = Foundation.Tensor.restrict (fun (x i : Fin a) => if i = x then 1 else 0) (fun (y : YIndex a h) (r : Fin h) => if rightY a h r = y then 1 else 0) (fun (z : ZIndex a h) (s : Fin (a + h - 1)) => if rightZ a h s = z then 1 else 0) (convolution K a h)

The right block is the zero extension along the translated coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_eq_extension {K : Type} [Field K] (a h : ℕ) : middleTensor K a h = Foundation.Tensor.restrict (fun (x i : Fin a) => if i.rev = x then 1 else 0) (fun (y : YIndex a h) (s : Fin (a + h - 1)) => if middleY a h s = y then 1 else 0) (fun (z : ZIndex a h) (r : Fin h) => if middleZ a h r = z then 1 else 0) (exchangedConvolution K a h)

The middle block is the zero extension of the exchanged convolution, with one reversible change of basis on its first leg.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.value_leftTensor {K : Type} [Field K] (χ : Character K) (a h : ℕ) : χ.value (leftTensor K a h) = χ.value (convolution K a h)

Every character assigns the left branch the value of C(a,h).

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.value_rightTensor {K : Type} [Field K] (χ : Character K) (a h : ℕ) : χ.value (rightTensor K a h) = χ.value (convolution K a h)

Translation of the outer coordinates preserves the right-branch value.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.value_middleTensor {K : Type} [Field K] (χ : Character K) (a h : ℕ) : χ.value (middleTensor K a h) = χ.value (exchangedConvolution K a h)

The middle-branch value is the value of the exchanged convolution tensor.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.exchangedConvolution_nonzero {K : Type} [Field K] {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : exchangedConvolution K a h ≠ 0

Exchanging two tensor legs preserves nonzeroness.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor_nonzero {K : Type} [Field K] {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : leftTensor K a h ≠ 0

The left retained branch is nonzero in every positive size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor_nonzero {K : Type} [Field K] {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : rightTensor K a h ≠ 0

The translated right branch is nonzero in every positive size.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor_nonzero {K : Type} [Field K] {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : middleTensor K a h ≠ 0

The exchanged middle branch is nonzero in every positive size.