Matrix entries indexed by tensor strings

Main definitions

• arrayL, arrayR: batch arrays with exactly m inner levels.
• leftStrOf, rightStrOf, outStrOf: entry strings.

Main results

• existsUnique_leftStr, existsUnique_rightStr, existsUnique_outStr: unique entry strings.

References

Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. These are finite mathematical counts and identities; they give no native program or instruction-cost certificate.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar.IsInner : LeftVar → Prop

Recognize the constructors .p i j as inner left variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar.IsInner : RightVar → Prop

Recognize the constructors .q i j as inner right variables.

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar.instDecidablePredIsInner : DecidablePred IsInner

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar.instDecidablePredIsInner : DecidablePred IsInner

def Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetL {L : ℕ} (u : LeftStr L) : Finset (Fin L)

Positions of the inner left variables in u.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetR {L : ℕ} (v : RightStr L) : Finset (Fin L)

Positions of the inner right variables in v.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetO {L : ℕ} (w : OutStr L) : Finset (Fin L)

Positions at which the output string is .z0.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.N0 (L m : ℕ) : ℕ

The outer dimension 3 ^ (L - m), with natural-number subtraction. In particular, this definition gives 1 if m > L.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.D (m : ℕ) : ℕ

The thin dimension 4 ^ m.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.K (L m : ℕ) : ℕ

The binomial coefficient L.choose m, counting size-m subsets of Fin L.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar.outerIndex : LeftVar → Fin 3

Extract i from .x i; return 0 on inner left variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar.innerIndex : LeftVar → Fin 2 × Fin 2

Extract (i, j) from .p i j; return (0, 0) on outer left variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar.outerIndex : RightVar → Fin 3

Extract j from .y j; return 0 on inner right variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar.innerIndex : RightVar → Fin 2 × Fin 2

Extract (i, j) from .q i j; return (0, 0) on outer right variables.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.rowIndex : OutVar → Fin 3

Extract the first index from .z i j; return 0 on .z0.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.colIndex : OutVar → Fin 3

Extract the second index from .z i j; return 0 on .z0.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.OuterStr (L m : ℕ) : Type

Functions from Fin (L - m) to Fin 3, used as outer row and column indices. Each value specifies the index of an outer left or right variable.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.InnerStr (m : ℕ) : Type

Functions from Fin m to pairs of Fin 2 indices, used for the common inner dimension of the two matrices. Left and right inner variables with the same pair of indices share one element of this type, so contraction over InnerStr m is ordinary matrix multiplication.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.outerPartL {L m : ℕ} (u : LeftStr L) (h : (innerSetL u).card = m) : OuterStr L m

Extract the outer left indices in increasing order of their positions, assuming u has exactly m inner positions.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.innerPartL {L m : ℕ} (u : LeftStr L) (h : (innerSetL u).card = m) : InnerStr m

Extract the inner left index pairs in increasing order of their positions, assuming u has exactly m inner positions.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.outerPartR {L m : ℕ} (v : RightStr L) (h : (innerSetR v).card = m) : OuterStr L m

The outer part of a right string whose inner set has m elements.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.innerPartR {L m : ℕ} (v : RightStr L) (h : (innerSetR v).card = m) : InnerStr m

The inner part of a right string whose inner set has m elements.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.rowO {L m : ℕ} (w : OutStr L) (h : (innerSetO w).card = m) : OuterStr L m

Read the first indices of the outer output variables in increasing position order, assuming w has exactly m inner positions.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.colO {L m : ℕ} (w : OutStr L) (h : (innerSetO w).card = m) : OuterStr L m

Read the second indices of the outer output variables in increasing position order, assuming w has exactly m inner positions.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftMat (L m : ℕ) : Type

Integer matrices with outer row indices and inner column indices.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.RightMat (L m : ℕ) : Type

Integer matrices with inner row indices and outer column indices.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.arrayL {L : ℕ} (m : ℕ) (X : Finset (Fin L) → LeftMat L m) : LeftStr L → ℤ

Encode a family of integer matrices as a left array. A string with exactly m inner positions selects X at that set of positions, with row outerPartL and column innerPartL; every other string has value zero.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.arrayR {L : ℕ} (m : ℕ) (Y : Finset (Fin L) → RightMat L m) : RightStr L → ℤ

Encode a family of integer matrices as a right array. A string with exactly m inner positions selects Y at that set of positions, with row innerPartR and column outerPartR; every other string has value zero.

The block-count parameter M

def Cslib.Algorithms.MatrixMultiplication.Schonhage.M (L m : ℕ) : ℕ

The quantity K L m * N0 L m ^ 2 used in the leaf and tile bounds.

Left, right and output strings with a given inner set, outer part and inner part

def Cslib.Algorithms.MatrixMultiplication.Schonhage.leftStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) : LeftStr L

The left string with inner set Q, outer part r and inner part π.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.rightStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) : RightStr L

The right string with inner set Q, inner part π and outer part c.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.outStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) : OutStr L

Construct an output string with .z0 at Q and .z (r k) (c k) at the k-th position of its complement. Both sets of positions use increasing order.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetL_leftStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) : innerSetL (leftStrOf Q hQ r π) = Q

The inner set of leftStrOf Q hQ r π is Q.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetR_rightStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) : innerSetR (rightStrOf Q hQ π c) = Q

The inner set of rightStrOf Q hQ π c is Q.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetO_outStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) : innerSetO (outStrOf Q hQ r c) = Q

The inner set of outStrOf Q hQ r c is Q.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outerPartL_leftStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) (h : (innerSetL (leftStrOf Q hQ r π)).card = m) : outerPartL (leftStrOf Q hQ r π) h = r

The outer part of leftStrOf Q hQ r π is r.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerPartL_leftStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) (h : (innerSetL (leftStrOf Q hQ r π)).card = m) : innerPartL (leftStrOf Q hQ r π) h = π

The inner part of leftStrOf Q hQ r π is π.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerPartR_rightStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) (h : (innerSetR (rightStrOf Q hQ π c)).card = m) : innerPartR (rightStrOf Q hQ π c) h = π

The inner part of rightStrOf Q hQ π c is π.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outerPartR_rightStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) (h : (innerSetR (rightStrOf Q hQ π c)).card = m) : outerPartR (rightStrOf Q hQ π c) h = c

The outer part of rightStrOf Q hQ π c is c.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.rowO_outStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) (h : (innerSetO (outStrOf Q hQ r c)).card = m) : rowO (outStrOf Q hQ r c) h = r

The row of outStrOf Q hQ r c is r.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.colO_outStrOf {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) (h : (innerSetO (outStrOf Q hQ r c)).card = m) : colO (outStrOf Q hQ r c) h = c

The column of outStrOf Q hQ r c is c.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.leftStr_eq_leftStrOf {L m : ℕ} {Q : Finset (Fin L)} (hQ : Q.card = m) {u : LeftStr L} (hu : innerSetL u = Q) (h : (innerSetL u).card = m) : u = leftStrOf Q hQ (outerPartL u h) (innerPartL u h)

A left string with inner set Q is the string leftStrOf of its outer part and its inner part.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.rightStr_eq_rightStrOf {L m : ℕ} {Q : Finset (Fin L)} (hQ : Q.card = m) {v : RightStr L} (hv : innerSetR v = Q) (h : (innerSetR v).card = m) : v = rightStrOf Q hQ (innerPartR v h) (outerPartR v h)

A right string with inner set Q is the string rightStrOf of its inner part and its outer part.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outStr_eq_outStrOf {L m : ℕ} {Q : Finset (Fin L)} (hQ : Q.card = m) {w : OutStr L} (hw : innerSetO w = Q) (h : (innerSetO w).card = m) : w = outStrOf Q hQ (rowO w h) (colO w h)

An output string with inner set Q is the string outStrOf of its row and its column.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.leftStrOf_inj {L m : ℕ} {Q : Finset (Fin L)} {hQ : Q.card = m} {r r' : OuterStr L m} {π π' : InnerStr m} : leftStrOf Q hQ r π = leftStrOf Q hQ r' π' ↔ r = r' ∧ π = π'

Left strings with the same inner set and different outer or inner parts are different.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outStrOf_inj {L m : ℕ} {Q : Finset (Fin L)} {hQ : Q.card = m} {Q' : Finset (Fin L)} {hQ' : Q'.card = m} {r c r' c' : OuterStr L m} : outStrOf Q hQ r c = outStrOf Q' hQ' r' c' ↔ Q = Q' ∧ r = r' ∧ c = c'

Output strings with different inner sets, rows or columns are different.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.existsUnique_leftStr {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) : ∃! u : LeftStr L, innerSetL u = Q ∧ ∃ (h : (innerSetL u).card = m), outerPartL u h = r ∧ innerPartL u h = π

For a set Q of cardinality m, an outer index r and an inner index π determine a unique left string with those extracted parts and inner set Q.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.existsUnique_rightStr {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) : ∃! v : RightStr L, innerSetR v = Q ∧ ∃ (h : (innerSetR v).card = m), innerPartR v h = π ∧ outerPartR v h = c

For a set Q of cardinality m, an inner index π and an outer index c determine a unique right string with those extracted parts and inner set Q.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.existsUnique_outStr {L m : ℕ} (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) : ∃! w : OutStr L, innerSetO w = Q ∧ ∃ (h : (innerSetO w).card = m), rowO w h = r ∧ colO w h = c

For a set Q of cardinality m, a row r and a column c determine a unique output string with those extracted indices and inner set Q.