Parameters of finite thin multiplication

Main results

• K_mul_N0_le_D_pow: bound K L m * N0 L m by D m ^ 18 at L = 19 * m.
• encoding_size_le: the shared encoding length bound.

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.K_le_pow (m : ℕ) : ↑(K (19 * m) m) ≤ (19 * Real.exp 1) ^ m

The binomial count at L = 19 * m is at most (19 * Real.exp 1) ^ m. This uses Nat.choose_le_exp_mul_div_pow and includes m = 0, when both sides are one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.nineteen_mul_exp_mul_three_pow_lt : 19 * Real.exp 1 * 3 ^ 18 < 4 ^ 18

The real constant 19 * exp 1 * 3 ^ 18 is strictly less than 4 ^ 18.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K_mul_N0_le_D_pow (m : ℕ) : K (19 * m) m * N0 (19 * m) m ≤ D m ^ 18

At L = 19 * m, the product K L m * N0 L m is at most D m ^ 18.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K_mul_N0_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : K (19 * m) m * N0 (19 * m) m ≤ N

The size condition D m ^ 18 ≤ N bounds K (19 * m) m * N0 (19 * m) m by N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.K0_mul_N0_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : K0 (19 * m) m * N0 (19 * m) m ≤ N

The size condition D m ^ 18 ≤ N bounds the band dimension at L = 19 * m by N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.padN_le_two_mul_of_D_pow_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : padN (19 * m) m N ≤ 2 * N

Under D m ^ 18 ≤ N, padding to complete bands at L = 19 * m gives a dimension at most 2 * N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.ten_pow_mul_two_rpow_div_three_pow_lt : 10 ^ 19 * 2 ^ (1 / 9) / 3 ^ 18 < 4 ^ 18

The real constant 10 ^ 19 * 2 ^ (1 / 9) / 3 ^ 18 is strictly less than 4 ^ 18.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.ten_pow_div_N0_le (m : ℕ) : 10 ^ (19 * m) * 2 ^ (↑m / 9) / ↑(N0 (19 * m) m) ≤ ↑(D m) ^ 18

At L = 19 * m, the real quotient 10 ^ L * 2 ^ (m / 9) / N0 L m is at most D m ^ 18.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encoding_size_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : 10 ^ (19 * m) ≤ 2 ^ (-↑m / 9) * ↑N * ↑(N0 (19 * m) m)

For L = 19 * m and D m ^ 18 ≤ N, the encoding index count 10 ^ L is at most 2 ^ (-m / 9) * N * N0 L m, as a real inequality (cf. [AlmanWilliams2026, equation (6)]).