Interval weights for the three-sector convolution degeneration

Section 5.2 assigns weights to the second and third coordinates of C(a, 3 * h + a - 1). The total weight is nonnegative on convolution support, and its zero set consists exactly of the three matching sector blocks. The middle block is a convolution with the last two legs exchanged and the first coordinate reversed.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.sourceWidth (a h : ℕ) : ℕ

Number of second-leg coordinates in the original convolution.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.sourceWidth a h = 3 * h + a - 1

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart (a h : ℕ) : ℕ

Beginning of the right sector on both the second and third legs.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightStart a h = 2 * h + a - 1

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.Support (a h i j k : ℕ) : Prop

A coefficient-one term of the original convolution tensor.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleY (a h j : ℕ) : Prop

The middle interval on the second tensor leg.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleZ (a h k : ℕ) : Prop

The middle interval on the third tensor leg.

Equations

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

@[instance_reducible]

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.instDecidableMiddleY (a h j : ℕ) : Decidable (MiddleY a h j)

Equations

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

@[instance_reducible]

instance MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.instDecidableMiddleZ (a h k : ℕ) : Decidable (MiddleZ a h k)

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.firstWeight (_i : ℕ) : ℤ

No weight is assigned to the common first leg.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.firstWeight _i = 0

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.secondWeight (a h j : ℕ) : ℤ

Weight one on the middle second-leg interval, zero elsewhere.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.thirdWeight (a h k : ℕ) : ℤ

Weight minus one on the middle third-leg interval, zero elsewhere.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight (a h i j k : ℕ) : ℤ

Exponent of the degeneration parameter on one term.

Equations

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

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MatchingSectors (a h j k : ℕ) : Prop

The three retained blocks have matching sector labels.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleY_of_middleZ {a h i j k : ℕ} (hs : Support a h i j k) (hz : MiddleZ a h k) : MiddleY a h j

A middle third-leg coordinate can only be reached from the middle second leg.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_zero_or_one {a h i j k : ℕ} (hs : Support a h i j k) : totalWeight a h i j k = 0 ∨ totalWeight a h i j k = 1

Every term has exponent zero or one, so no negative powers occur.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_nonneg {a h i j k : ℕ} (hs : Support a h i j k) : 0 ≤ totalWeight a h i j k

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_zero_iff {a h i j k : ℕ} (hs : Support a h i j k) : totalWeight a h i j k = 0 ↔ MatchingSectors a h j k

The constant coefficient consists exactly of the three matching blocks.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.totalWeight_eq_one_iff {a h i j k : ℕ} (hs : Support a h i j k) : totalWeight a h i j k = 1 ↔ MiddleY a h j ∧ ¬MiddleZ a h k

Only a middle second-leg coordinate paired with an outer third-leg coordinate is erased by the degeneration.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch (a h i j k : ℕ) : Prop

Parametrization of the left copy of C(a,h).

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch a h i j k = ∃ (u : ℕ) (r : ℕ), u < a ∧ r < h ∧ i = u ∧ j = r ∧ k = u + r

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch (a h i j k : ℕ) : Prop

Parametrization of the middle copy with the second and third legs exchanged.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch a h i j k = ∃ (u : ℕ) (r : ℕ), u < a ∧ r < h ∧ i = a - 1 - u ∧ j = h + u + r ∧ k = h + a - 1 + r

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch (a h i j k : ℕ) : Prop

Parametrization of the right translated copy of C(a,h).

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) : LeftBranch a h i j k ↔ j < h ∧ k < h + a - 1

The left block preserves the actual first coordinate.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) : MiddleBranch a h i j k ↔ MiddleY a h j ∧ MiddleZ a h k

The middle support equation becomes convolution after reversing the first coordinate and exchanging the second and third legs.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightBranch_iff {a h i j k : ℕ} (hs : Support a h i j k) : RightBranch a h i j k ↔ rightStart a h ≤ j ∧ rightStart a h ≤ k

The right block is the same convolution after translating the two outer coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.left_support_coordinates {a h i r s : ℕ} (hi : i < a) (hr : r < h) : Support a h i r s ↔ s = i + r

On the left coordinate block, the support equation is the ordinary convolution equation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.right_support_coordinates {a h i r s : ℕ} (hi : i < a) (hr : r < h) : Support a h i (rightStart a h + r) (rightStart a h + s) ↔ s = i + r

Translation of the right block preserves the convolution equation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middle_support_coordinates {a h i s r : ℕ} (hi : i < a) (hr : r < h) : Support a h i (h + s) (h + a - 1 + r) ↔ s = a - 1 - i + r

In middle-block coordinates the support equation is convolution with the first coordinate reversed and the other two coordinates exchanged.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.retained_support_iff {a h i j k : ℕ} (hs : Support a h i j k) : totalWeight a h i j k = 0 ↔ LeftBranch a h i j k ∨ MiddleBranch a h i j k ∨ RightBranch a h i j k

Exact retained support of the three-sector degeneration.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.LeftBranch.support {a h i j k : ℕ} (hb : LeftBranch a h i j k) : Support a h i j k

Every displayed left-branch term belongs to the original convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.MiddleBranch.support {a h i j k : ℕ} (hb : MiddleBranch a h i j k) : Support a h i j k

Every displayed middle-branch term belongs to the original convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.RightBranch.support {a h i j k : ℕ} (hb : RightBranch a h i j k) : Support a h i j k

Every displayed right-branch term belongs to the original convolution.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.support_and_weight_zero_iff (a h i j k : ℕ) : Support a h i j k ∧ totalWeight a h i j k = 0 ↔ LeftBranch a h i j k ∨ MiddleBranch a h i j k ∨ RightBranch a h i j k

Exact equality of the retained support and the three explicitly parametrized convolution branches, without a pre-existing support assumption.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.reverse_reverse {a u : ℕ} (hu : u < a) : a - 1 - (a - 1 - u) = u

The first-coordinate reversal is involutive on its natural range.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_coordinates_unique {a h i k u r u' r' : ℕ} (hu : u < a) (hu' : u' < a) (hi : i = a - 1 - u) (hi' : i = a - 1 - u') (hk : k = h + a - 1 + r) (hk' : k = h + a - 1 + r') : u = u' ∧ r = r'

The middle branch has unique reversed-convolution coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_not_middleBranch {a h i j k : ℕ} (hl : LeftBranch a h i j k) : ¬MiddleBranch a h i j k

The left and middle branches use disjoint second-leg coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_not_rightBranch {a h i j k : ℕ} (hl : LeftBranch a h i j k) : ¬RightBranch a h i j k

The left and right branches use disjoint second-leg coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_not_rightBranch {a h i j k : ℕ} (hm : MiddleBranch a h i j k) : ¬RightBranch a h i j k

The middle and right branches use disjoint second-leg coordinates.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.leftBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : ∃ (i : ℕ) (j : ℕ) (k : ℕ), LeftBranch a h i j k

Positivity of the two original dimensions makes the left branch nonempty.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.middleBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : ∃ (i : ℕ) (j : ℕ) (k : ℕ), MiddleBranch a h i j k

Positivity makes the exchanged middle branch nonempty as well.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.rightBranch_nonempty {a h : ℕ} (ha : 0 < a) (hh : 0 < h) : ∃ (i : ℕ) (j : ℕ) (k : ℕ), RightBranch a h i j k

Positivity also makes the translated right branch nonempty.