Padding and tiling correctness

Main results

• nonempty_layout: valid layouts exist whenever m ≤ L.
• Full.bandArray_eq_mul: product entries as Full.result values of band arrays.
• outStrOfPos_injective: positions in a tile have distinct output 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.

The numbers

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K0_sq_le_K (L m : ℕ) : K0 L m ^ 2 ≤ K L m

The square of the natural square root K0 L m is at most K L m.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K_le_four_mul_K0_sq (L m : ℕ) : K L m ≤ 4 * K0 L m ^ 2

The binomial count K L m is at most four times K0 L m ^ 2.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandSize_pos {L m : ℕ} (hmL : m ≤ L) : 0 < bandSize L m

A band has at least one row.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandSize_dvd_padN (L m N : ℕ) : bandSize L m ∣ padN L m N

The padded dimension is a multiple of the band size.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.le_padN {L m : ℕ} (hmL : m ≤ L) (N : ℕ) : N ≤ padN L m N

For m ≤ L, padding covers all N original positions. The parameter condition ensures a positive band size.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.padN_lt_add_bandSize {L m : ℕ} (hmL : m ≤ L) (N : ℕ) : padN L m N < N + bandSize L m

For m ≤ L, the padded dimension is strictly less than N + bandSize L m, including N = 0.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.padN_le_two_mul (L m N : ℕ) (hN : K0 L m * N0 L m ≤ N) : padN L m N ≤ 2 * N

If the band size is at most N, the padded dimension is at most 2 * N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_tiles (L m N : ℕ) : (tiles L m N).card = numBands L m N ^ 2

The number of tiles is the square of the number of bands.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_tiles_mul_M_le (L m N : ℕ) : (tiles L m N).card * M L m ≤ 4 * padN L m N ^ 2

The tile count multiplied by M L m is at most 4 * padN L m N ^ 2. The bound is stated without division and requires no positivity hypothesis.

The table of subsets and the matrices of a tile

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.nonempty_layout {L m : ℕ} (hmL : m ≤ L) : Nonempty (Layout L m)

Indexing data Layout L m exist for every m ≤ L, including m = 0.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyL_table {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (β : ℕ) (g h : Fin (K0 L m)) : bandFamilyL lay X β (lay.table (g, h)) = rowBlock lay X (β * K0 L m + ↑g)

At the table entry (g, h), the left family selects row block β * K0 L m + g.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyR_table {L m N : ℕ} (lay : Layout L m) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (β : ℕ) (g h : Fin (K0 L m)) : bandFamilyR lay Y β (lay.table (g, h)) = colBlock lay Y (β * K0 L m + ↑h)

The matrix Y_Q of the block product in position (g, h) is the h-th column block of the column band.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyL_eq_zero {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (β : ℕ) {Q : Finset (Fin L)} (hQ : ∀ (gh : Fin (K0 L m) × Fin (K0 L m)), lay.table gh ≠ Q) : bandFamilyL lay X β Q = 0

The left family is zero at any level set outside the table image.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandFamilyR_eq_zero {L m N : ℕ} (lay : Layout L m) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (β : ℕ) {Q : Finset (Fin L)} (hQ : ∀ (gh : Fin (K0 L m) × Fin (K0 L m)), lay.table gh ≠ Q) : bandFamilyR lay Y β Q = 0

The right family is zero at any level set outside the table image.

Product identities for tile arrays

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.bandArray_eq_block_mul {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (β β' : ℕ) (g h : Fin (K0 L m)) (r c : OuterStr L m) : result L (bandArrayL lay X β) (bandArrayR lay Y β') (outStrOf (lay.table (g, h)) ⋯ r c) = (rowBlock lay X (β * K0 L m + ↑g) * colBlock lay Y (β' * K0 L m + ↑h)) r c

For the band arrays of tile (β, β'), Full.result at the output string for table entry (g, h) equals the product entry of row block β * K0 L m + g and column block β' * K0 L m + h.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.bandArray_eq_mul {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (I J : Fin N) : result L (bandArrayL lay X (bandOf L m ↑I)) (bandArrayR lay Y (bandOf L m ↑J)) (outStrOfPos lay ↑I ↑J) = (X * Y) I J

The band arrays for the tile containing an original position (I, J) give Full.result equal to (X * Y) I J at outStrOfPos lay I J. The matrices may have arbitrary signed integer entries.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bilinearProduct_bandArray_eq_mul {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (I J : Fin N) : bilinearProduct (bandArrayL lay X (bandOf L m ↑I)) (bandArrayR lay Y (bandOf L m ↑J)) (outStrOfPos lay ↑I ↑J) = (X * Y) I J

At the output string of an original position (I, J), the bilinear product of its two band arrays equals (X * Y) I J.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandOf_lt_numBands {L m : ℕ} (hmL : m ≤ L) (N I : ℕ) (hI : I < N) : bandOf L m I < numBands L m N

For m ≤ L, any index I < N has band index below numBands L m N.

The output string of a position

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.innerSetO_outStrOfPos {L m : ℕ} (lay : Layout L m) (I J : ℕ) : innerSetO (outStrOfPos lay I J) = lay.table (blockOf lay I, blockOf lay J)

The inner set of a position's output string is the table entry indexed by its two within-band block indices.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_innerSetO_outStrOfPos {L m : ℕ} (lay : Layout L m) (I J : ℕ) : (innerSetO (outStrOfPos lay I J)).card = m

The inner set of the output string of a position has exactly m elements.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outStrOfPos_injective {L m : ℕ} (lay : Layout L m) (I J I' J' : ℕ) (hI : bandOf L m I = bandOf L m I') (hJ : bandOf L m J = bandOf L m J') (h : outStrOfPos lay I J = outStrOfPos lay I' J') : I = I' ∧ J = J'

Within a fixed pair of row and column bands, equality of output strings implies equality of both natural-number position indices.