Finite thin-product correctness and cardinality bounds

Main results

• thin_product_spec: exact queried entries for arbitrary signed integer matrices.
• encodings_total_le, total_leaves_le, total_passed_sets_le: explicit finite totals.

Correctness holds for arbitrary signed integer matrices and any layout. For D = 4^m, L = 19m, D^18 ≤ N and W.card * 2^m ≤ N², the encoding entry count is at most 4 * D^(-1/18) * N², the sum of contributing-leaf cardinalities is at most 33 * D^(-1/18) * N², and the sum of passed request-set cardinalities is at most (19m + 1) * 33 * D^(-1/18) * N². Here N is the original matrix dimension. The definitions permit zero parameters and empty request sets; the bounds retain their stated size and sparsity hypotheses. No native program or instruction bound is proved.

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.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.tile_mem_tiles {L m N : ℕ} (hmL : m ≤ L) (I J : Fin N) : (bandOf L m ↑I, bandOf L m ↑J) ∈ tiles L m N

For m ≤ L, the band pair of any position (I, J) : Fin N × Fin N belongs to the finite tile set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.outStrOfPos_mem_wantedStrings {L m N : ℕ} (lay : Layout L m) (W : Finset (Fin N × Fin N)) {I J : Fin N} (hIJ : (I, J) ∈ W) : outStrOfPos lay ↑I ↑J ∈ wantedStrings lay W (bandOf L m ↑I) (bandOf L m ↑J)

A requested position contributes its output string to wantedStrings for its band pair.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_innerSetO_of_mem_wantedStrings {L m N : ℕ} (lay : Layout L m) (W : Finset (Fin N × Fin N)) (β β' : ℕ) (w : OutStr L) (hw : w ∈ wantedStrings lay W β β') : (innerSetO w).card = m

Every string requested in a tile has exactly m inner positions.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.thin_product_spec {L m N : ℕ} (lay : Layout L m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (W : Finset (Fin N × Fin N)) (I J : Fin N) (hIJ : (I, J) ∈ W) : Pruned.result L (encodingL (bandArrayL lay X (bandOf L m ↑I))) (encodingR (bandArrayR lay Y (bandOf L m ↑J))) (wantedStrings lay W (bandOf L m ↑I) (bandOf L m ↑J)) (outStrOfPos lay ↑I ↑J) = (X * Y) I J

For arbitrary signed integer matrices of shapes N × D m and D m × N, the pruned result at any position in W equals the corresponding entry of X * Y. The encodings and request set are those for that position's row and column bands. This holds for every Layout L m, which includes m ≤ L, without the size or sparsity conditions used in the counting bounds (cf. [AlmanWilliams2026, Theorem 5]).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.le_sq_div_sqrt_D_iff (m N w : ℕ) : ↑w ≤ ↑N ^ 2 / √↑(D m) ↔ w * 2 ^ m ≤ N ^ 2

The real inequality w ≤ N² / sqrt (D m) is equivalent to the natural-number inequality w * 2 ^ m ≤ N ^ 2, including m = 0.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encodings_total_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : ↑(2 * numBands (19 * m) m N * 10 ^ (19 * m)) ≤ 4 * ↑(D m) ^ (-(1 / 18)) * ↑N ^ 2

At L = 19 * m with D m ^ 18 ≤ N, the encodings of all row-band and column-band arrays have at most 4 * D^(-1/18) * N² entries in total, where D = D m. The counted quantity is 2 * numBands L m N * 10 ^ L, and N is the original dimension. This is an entry count, not a bound on instructions or encoding time.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_card_wantedStrings_le {L m N : ℕ} (lay : Layout L m) (W : Finset (Fin N × Fin N)) : ∑ T ∈ tiles L m N, (wantedStrings lay W T.1 T.2).card ≤ W.card

Summing the cardinalities of the requested-string sets over all tiles gives at most W.card.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_M_le (L m N : ℕ) : ∑ _T ∈ tiles L m N, M L m ≤ 4 * padN L m N ^ 2

The sum of M L m over the finite tile set is at most 4 * padN L m N ^ 2.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_card_leaves_le {m N : ℕ} (lay : Layout (19 * m) m) (W : Finset (Fin N × Fin N)) : ↑(∑ T ∈ tiles (19 * m) m N, (leaves (wantedStrings lay W T.1 T.2)).card) ≤ saving m * (2 ^ m * ↑W.card + 2 * ↑(∑ _T ∈ tiles (19 * m) m N, M (19 * m) m))

At L = 19 * m, bound the sum of contributing-leaf cardinalities for the tile request sets by saving m * (2 ^ m * W.card + 2 * ∑ T ∈ tiles L m N, M L m). A leaf used in distinct tiles is counted once for each such tile.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.total_leaves_le {m N : ℕ} (lay : Layout (19 * m) m) (W : Finset (Fin N × Fin N)) (hN : D m ^ 18 ≤ N) (hW : W.card * 2 ^ m ≤ N ^ 2) : ↑(∑ T ∈ tiles (19 * m) m N, (leaves (wantedStrings lay W T.1 T.2)).card) ≤ 33 * ↑(D m) ^ (-(1 / 18)) * ↑N ^ 2

At L = 19 * m, assume D m ^ 18 ≤ N and W.card * 2 ^ m ≤ N ^ 2. The sum of contributing-leaf cardinalities over all tiles is then at most 33 * D^(-1/18) * N², where D = D m and N is the original dimension. This counts leaves with their tile multiplicities, not executed instructions.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.total_passed_sets_le {m N : ℕ} (lay : Layout (19 * m) m) (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) (W : Finset (Fin N × Fin N)) (hN : D m ^ 18 ≤ N) (hW : W.card * 2 ^ m ≤ N ^ 2) : ↑(∑ T ∈ tiles (19 * m) m N, Pruned.totalSize (encodingL (bandArrayL lay X T.1)) (encodingR (bandArrayR lay Y T.2)) (wantedStrings lay W T.1 T.2)) ≤ ↑(19 * m + 1) * (33 * ↑(D m) ^ (-(1 / 18)) * ↑N ^ 2)

At L = 19 * m, assume D m ^ 18 ≤ N and W.card * 2 ^ m ≤ N ^ 2. Summing Pruned.totalSize over all tiles gives at most (19 * m + 1) * (33 * D^(-1/18) * N²), where D = D m and N is the original dimension. The quantity sums request-set cardinalities through the pruned recursions; it is not an instruction count.