The actual three-sector polynomial degeneration

The interval weights of SectorWeights act by diagonal local maps on the coefficient tensor C(a, 3h+a-1). Shifting every third-leg weight by one makes the local maps polynomial. Their restriction is exactly X * retained + X^2 * erased, so the existing polynomial-restriction degeneration interface applies with leading order one and local degree bounds (0,1,1).

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex (a h : ℕ) : Type

Second-leg coordinates of the three-sector source tensor.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.YIndex a h = Fin (MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.sourceWidth a h)

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.ZIndex (a h : ℕ) : Type

Third-leg coordinates of the three-sector source tensor.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.source (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The source coefficient tensor, with its actual shared first-input space.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.source_ne_zero_iff {K : Type} [Field K] {a h : ℕ} (i : Fin a) (j : YIndex a h) (k : ZIndex a h) : source K a h i j k ≠ 0 ↔ Support a h ↑i ↑j ↑k

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.retained (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The weight-zero part in the original coordinate spaces.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.erased (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The positive-weight part, all of whose supported terms have weight one.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftTensor (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The left retained branch, still in the common ambient coordinate spaces.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleTensor (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The middle retained branch; its first leg is the actual shared first leg.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightTensor (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The right retained branch in the original coordinate spaces.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.retained_eq_three_branches {K : Type} [Field K] (a h : ℕ) : retained K a h = leftTensor K a h + middleTensor K a h + rightTensor K a h

The retained tensor is exactly the sum of the three stated branches, with coefficient one on each and the original first-leg coordinates shared.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.source_eq_retained_add_erased {K : Type} [Field K] (a h : ℕ) : source K a h = retained K a h + erased K a h

Every source term belongs either to the retained tensor or the erased one.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor (Polynomial K) (Fin a) (YIndex a h) (ZIndex a h)

The normalized polynomial family appearing in the unshifted weights.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap (K : Type) [Field K] (a : ℕ) (output input : Fin a) : Polynomial K

The first local map fixes the common input basis.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap K a output input = if input = output then 1 else 0

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap (K : Type) [Field K] (a h : ℕ) (output input : YIndex a h) : Polynomial K

The second local map assigns weight one to the middle interval.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightMap (K : Type) [Field K] (a h : ℕ) (output input : ZIndex a h) : Polynomial K

Shift the third-leg weights by one, giving weight zero to the middle interval and weight one to the two outer intervals.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial (K : Type) [Field K] (a h : ℕ) : Foundation.Tensor (Polynomial K) (Fin a) (YIndex a h) (ZIndex a h)

One simultaneous polynomial restriction of the whole source tensor.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_apply {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) : polynomial K a h i j k = ((if MiddleY a h ↑j then Polynomial.X else 1) * if MiddleZ a h ↑k then 1 else Polynomial.X) * Polynomial.C (source K a h i j k)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_identity {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) : polynomial K a h i j k = Polynomial.X * Polynomial.C (retained K a h i j k) + Polynomial.X ^ 2 * Polynomial.C (erased K a h i j k)

The shifted polynomial restriction has precisely two possible degrees.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_eq_X_mul_normalized {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) : polynomial K a h i j k = Polynomial.X * normalizedPolynomial K a h i j k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.polynomial_coeff {K : Type} [Field K] (a h : ℕ) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) (n : ℕ) : (polynomial K a h i j k).coeff n = (if n = 1 then retained K a h i j k else 0) + if n = 2 then erased K a h i j k else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftMap_degree {K : Type} [Field K] (a : ℕ) (output input : Fin a) : (leftMap K a output input).degree ≤ 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleMap_degree {K : Type} [Field K] (a h : ℕ) (output input : YIndex a h) : (middleMap K a h output input).degree ≤ 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightMap_degree {K : Type} [Field K] (a h : ℕ) (output input : ZIndex a h) : (rightMap K a h output input).degree ≤ 1

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.restriction (K : Type) [Field K] (a h : ℕ) : (source K a h).PolynomialRestrictionDegeneration (retained K a h) 1 0 1 1

The three-sector construction is an actual polynomial restriction degeneration in the existing tensor API, with leading order one.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.restriction_basePolynomial {K : Type} [Field K] (a h : ℕ) : (restriction K a h).basePolynomial = polynomial K a h

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial_eval {K : Type} [Field K] (a h : ℕ) (t : K) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) : Polynomial.eval t (normalizedPolynomial K a h i j k) = retained K a h i j k + t * erased K a h i j k

Evaluation of the normalized family has exactly the paper's form.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.normalizedPolynomial_eval_restriction {K : Type} [Field K] (a h : ℕ) (t : K) (ht : t ≠ 0) : (fun (i : Fin a) (j : YIndex a h) (k : ZIndex a h) => Polynomial.eval t (normalizedPolynomial K a h i j k)) = Foundation.Tensor.restrict (fun (output input : Fin a) => if input = output then t⁻¹ else 0) (fun (output input : YIndex a h) => Polynomial.eval t (middleMap K a h output input)) (fun (output input : ZIndex a h) => Polynomial.eval t (rightMap K a h output input)) (source K a h)

At nonzero parameters, the unshifted normalized polynomial is still an ordinary restriction: divide the first local map by the parameter.