The tensor map with L copies

The branches have a common first coordinate space and common sizes on the other two legs. Their second and third coordinates carry a matching sector label. The three maps below are independent linear substitutions on the three legs of L complete copies of the source tensor. The paper takes L = 5M; here L is any period with 3(M - 1) < L that is nonzero in the coefficient field.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sectorNumber {M : ℕ} (i : Fin M) : ℤ

The paper numbers sectors from one, while Fin M numbers them from zero.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sectorNumber i = ↑↑i + 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sectorNumber_bounds {M : ℕ} (i : Fin M) : 1 ≤ sectorNumber i ∧ sectorNumber i ≤ ↑M

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sectorNumber_injective {M : ℕ} : Function.Injective sectorNumber

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor {K : Type} [Field K] {M : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor K X (Fin M × Y) (Fin M × Z)

Branches sharing X, with matching and disjoint Y and Z sectors.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor B x y z = if y.1 = z.1 then B y.1 x y.2 z.2 else 0

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.firstProjectionMap {K : Type} [Field K] {M L : ℕ} {X : Type u_1} (ζ : K) : X × Fin M → Fin L × X → K

The first local Fourier substitution guesses the missing sector.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.secondProjectionMap {K : Type} [Field K] {M L : ℕ} {Y : Type u_2} (ζ : K) : (Fin M × Y) × Fin M → Fin L × Fin M × Y → K

The second local map knows the sector through its original coordinate.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.thirdProjectionMap {K : Type} [Field K] {M L : ℕ} {Z : Type u_3} (ζ : K) : (Fin M × Z) × Fin M → Fin L × Fin M × Z → K

The third local map carries the single Fourier normalization factor.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.projectedTensor {K : Type} [Field K] {M : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (L : ℕ) (ζ : K) (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor K (X × Fin M) ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M)

The exact coefficient tensor after Fourier projection, before weighting.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finiteProjection_restrict {K : Type} [Field K] {M L : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (ζ : K) (hζ : ζ ≠ 0) (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor.restrict (firstProjectionMap ζ) (secondProjectionMap ζ) (thirdProjectionMap ζ) (Foundation.Tensor.directSum fun (x : Fin L) => sharedFirstTensor B) = projectedTensor L ζ B

The L copies and the three explicit local Fourier maps realize the projected tensor by an ordinary restriction.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationPolynomial {K : Type} [Field K] {M : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (L : ℕ) (ζ : K) (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor (Polynomial K) (X × Fin M) ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M)

The polynomial after the Fourier projection and square weighting.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationTarget {K : Type} [Field K] {M : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor K (X × Fin M) ((Fin M × Y) × Fin M) ((Fin M × Z) × Fin M)

The surviving tensor: sector labels match on all three legs, while the additional second/third coordinates form a dot product.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationTarget B x y z = if x.2 = y.1.1 ∧ y.1.1 = z.1.1 ∧ y.2 = z.2 then B y.1.1 x.1 y.1.2 z.1.2 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_coeff_zero {K : Type} [Field K] {M L : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ζ : K} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (B : Fin M → Foundation.Tensor K X Y Z) : (fun (x : X × Fin M) (y : (Fin M × Y) × Fin M) (z : (Fin M × Z) × Fin M) => (separationPolynomial L ζ B x y z).coeff 0) = separationTarget B

The square-weighted polynomial has exactly the advertised constant tensor.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_degree {K : Type} [Field K] {M L : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {ζ : K} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (B : Fin M → Foundation.Tensor K X Y Z) (x : X × Fin M) (y : (Fin M × Y) × Fin M) (z : (Fin M × Z) × Fin M) : (separationPolynomial L ζ B x y z).degree ≤ ↑((M - 1) ^ 2)

Its degree is bounded for each fixed finite separation construction.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.firstSeparationMap {K : Type} [Field K] {M L : ℕ} {X : Type u_1} (ζ t : K) (x : X × Fin M) (r : Fin L × X) : K

The first local Fourier map followed by its integer weight.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.secondSeparationMap {K : Type} [Field K] {M L : ℕ} {Y : Type u_2} (ζ t : K) (y : (Fin M × Y) × Fin M) (r : Fin L × Fin M × Y) : K

The second local Fourier map followed by its possibly negative weight.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.thirdSeparationMap {K : Type} [Field K] {M L : ℕ} {Z : Type u_3} (ζ t : K) (z : (Fin M × Z) × Fin M) (r : Fin L × Fin M × Z) : K

The third local Fourier map followed by its possibly negative weight.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.weightedProjection_restrict {K : Type} [Field K] {M L : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] (ζ t : K) (hζ : ζ ≠ 0) (B : Fin M → Foundation.Tensor K X Y Z) : Foundation.Tensor.restrict (firstSeparationMap ζ t) (secondSeparationMap ζ t) (thirdSeparationMap ζ t) (Foundation.Tensor.directSum fun (x : Fin L) => sharedFirstTensor B) = fun (x : X × Fin M) (y : (Fin M × Y) × Fin M) (z : (Fin M × Z) × Fin M) => t ^ firstWeight (sectorNumber x.2) * t ^ secondWeight (sectorNumber y.1.1) (sectorNumber y.2) * t ^ thirdWeight (sectorNumber z.1.1) (sectorNumber z.2) * projectedTensor L ζ B x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationPolynomial_eval {K : Type} [Field K] {M L : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {ζ : K} (hM : 0 < M) (hL : ↑L ≠ 0) (hLM : 3 * M < L + 3) (hζ : IsPrimitiveRoot ζ L) (B : Fin M → Foundation.Tensor K X Y Z) (t : K) (ht : t ≠ 0) : (fun (x : X × Fin M) (y : (Fin M × Y) × Fin M) (z : (Fin M × Z) × Fin M) => Polynomial.eval t (separationPolynomial L ζ B x y z)) = Foundation.Tensor.restrict (firstSeparationMap ζ t) (secondSeparationMap ζ t) (thirdSeparationMap ζ t) (Foundation.Tensor.directSum fun (x : Fin L) => sharedFirstTensor B)

At every nonzero parameter the polynomial tensor is an ordinary restriction of exactly L complete source copies.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationFirstEquiv {M : ℕ} {X : Type u_1} : X × Fin M ≃ Fin M × X × Unit

The first-leg relabeling adds the trivial first coordinate of the dot product.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationSideEquiv {M : ℕ} (A : Type u_4) : (Fin M × A) × Fin M ≃ Fin M × A × Fin M

The other two relabelings merely reassociate their coordinates.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationSideEquiv A = Equiv.prodAssoc (Fin M) A (Fin M)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.separationTarget_eq_directSum {K : Type} [Field K] {M : ℕ} {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (B : Fin M → Foundation.Tensor K X Y Z) : separationTarget B = Foundation.Tensor.pullback (⇑separationFirstEquiv) (⇑(separationSideEquiv Y)) (⇑(separationSideEquiv Z)) (Foundation.Tensor.directSum fun (h : Fin M) => (B h).product (Foundation.Tensor.dotPairing (Fin M)).cyclic.cyclic)

The separated target, expressed as a genuine full direct sum of products.