Tiling layout data

Main definitions

• Layout: index equivalences and an injective assignment of level sets to block pairs.
• wantedStrings, tiles: requested outputs grouped by tile.

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.K0 (L m : ℕ) : ℕ

The natural square root of the number K L m of size-m level sets.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.N0_pos (L m : ℕ) : 0 < N0 L m

N₀ = 3^{L-m} is positive.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K0_pos {L m : ℕ} (h : m ≤ L) : 0 < K0 L m

K₀ = ⌊√binom(L, m)⌋ is positive when m ≤ L.

structure Cslib.Algorithms.MatrixMultiplication.Schonhage.Layout (L m : ℕ) : Type

Indexing data for the block decomposition, under m ≤ L.

The three equivalences identify block rows, block columns and the thin dimension with their string indices. The injective table assigns a size-m subset of Fin L to each pair of block indices in a tile. All tiles use this same table. The structure contains no matrix values or solver certificate; the correctness results hold for any such indexing choices.

• hmL : m ≤ L
• rowIdx : Fin (N0 L m) ≃ OuterStr L m

  Index a block's rows by outer strings.

• colIdx : Fin (N0 L m) ≃ OuterStr L m

  Index a block's columns by outer strings.

• innerIdx : Fin (D m) ≃ InnerStr m

  Index the thin matrix dimension by strings of inner index pairs.

• table : Fin (K0 L m) × Fin (K0 L m) → Finset (Fin L)

  Assign a distinct size-m level set to each block product in a tile.

• table_card (gh : Fin (K0 L m) × Fin (K0 L m)) : (self.table gh).card = m
• table_injective : Function.Injective self.table

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

The common band dimension K0 L m * N0 L m: each band contains K0 L m consecutive blocks of size N0 L m.

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

The quotient (N + bandSize L m - 1) / bandSize L m. When m ≤ L, the band size is positive and this is the number of bands needed to cover N positions, including N = 0.

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

The dimension covered by numBands L m N complete bands.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.padRows {N D' : ℕ} (X : Matrix (Fin N) (Fin D') ℤ) (I : ℕ) (k : Fin D') : ℤ

Extend X to natural-number row indices by returning zero at indices I ≥ N.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.padCols {N D' : ℕ} (Y : Matrix (Fin D') (Fin N) ℤ) (k : Fin D') (J : ℕ) : ℤ

Extend Y to natural-number column indices by returning zero at indices J ≥ N.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.rowBlock {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (B : ℕ) : LeftMat L m

Extract the N0 L m rows starting at B * N0 L m from padRows X, using lay.rowIdx and lay.innerIdx to index the resulting integer matrix by strings.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.colBlock {L m N : ℕ} (lay : Layout L m) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (B : ℕ) : RightMat L m

Extract the N0 L m columns starting at B * N0 L m from padCols Y, using lay.innerIdx and lay.colIdx to index the resulting integer matrix by strings.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyL {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (β : ℕ) : Finset (Fin L) → LeftMat L m

For a table entry Q = lay.table (g, h), select row block β * K0 L m + g of X; return the zero matrix for sets outside the table's image. Injectivity of the table ensures that the defining sum selects at most one matrix.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyR {L m N : ℕ} (lay : Layout L m) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (β : ℕ) : Finset (Fin L) → RightMat L m

For a table entry Q = lay.table (g, h), select column block β * K0 L m + h of Y; return the zero matrix for sets outside the table's image.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.bandArrayL {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (β : ℕ) : LeftStr L → ℤ

The left batch array formed from the block family for row band β.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.bandArrayR {L m N : ℕ} (lay : Layout L m) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (β : ℕ) : RightStr L → ℤ

The right batch array formed from the block family for column band β.

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

The band that contains row (or column) I.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.blockOf {L m : ℕ} (lay : Layout L m) (I : ℕ) : Fin (K0 L m)

The position, within its band, of the block that contains row (or column) I.

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

The position of row (or column) I within its block.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.outStrOfPos {L m : ℕ} (lay : Layout L m) (I J : ℕ) : OutStr L

Encode the within-tile position (I, J) as an output string. Its inner set comes from the table at the two block indices, and its outer indices come from the two offsets within those blocks. The tile itself is identified separately by (bandOf L m I, bandOf L m J).

def Cslib.Algorithms.MatrixMultiplication.Schonhage.wantedStrings {L m N : ℕ} (lay : Layout L m) (W : Finset (Fin N × Fin N)) (β β' : ℕ) : Finset (OutStr L)

Output strings for the positions of W whose row band is β and column band is β'. This is the image of the filtered position set under outStrOfPos lay.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.tiles (L m N : ℕ) : Finset (ℕ × ℕ)

All the tiles: pairs of a row band and a column band.