Magnitudes of specified integer values and auxiliary counts

Main results

• abs_bandArrayL_le, abs_bandArrayR_le: input entries are unchanged or zero.
• abs_encodingL_le, abs_encodingR_le, Pruned.abs_result_le: explicit integer magnitude bounds.
• minutiae_total_le: bound on layout subsets, tiles and wanted positions.

The magnitude bounds concern band-array values, encoded values and returned pruned values. They do not bound every intermediate state of a native implementation or certify a machine word width.

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.

Auxiliary finite counts

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

When D m ^ 18 ≤ N, the number K (19 * m) m of size-m level sets is at most N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_tiles_mul_N0_le {L m : ℕ} (hmL : m ≤ L) (N : ℕ) : (tiles L m N).card * N0 L m ≤ 4 * padN L m N ^ 2

For m ≤ L, the tile count multiplied by N0 L m is at most four times the square of the padded dimension padN L m N.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.two_rpow_le_of_D_pow_le (m N : ℕ) (hN : D m ^ 18 ≤ N) : 2 ^ (↑m / 9) ≤ ↑N

The size condition D m ^ 18 ≤ N implies the real bound 2 ^ (m / 9) ≤ N.

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

At L = 19 * m, the outer dimension is at least the real power 2 ^ (m / 9).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.minutiae_total_le (m N : ℕ) (W : Finset (Fin N × Fin N)) (hN : D m ^ 18 ≤ N) (hW : W.card * 2 ^ m ≤ N ^ 2) : ↑(K (19 * m) m + (tiles (19 * m) m N).card + W.card) ≤ 18 * ↑(D m) ^ (-(1 / 18)) * ↑N ^ 2

At L = 19 * m, the sum of K L m, the tile count and W.card is at most 18 * D^(-1/18) * N², where D = D m and N is the original matrix dimension. The hypotheses are D m ^ 18 ≤ N and W.card * 2 ^ m ≤ N ^ 2. This counts finite objects; it does not count operations on them.

Bounds on specified integer values

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_bandArrayL_le {L m N : ℕ} (lay : Layout L m) {X : Matrix (Fin N) (Fin (D m)) ℤ} {A : ℤ} (hA : 0 ≤ A) (hX : ∀ (I : Fin N) (k : Fin (D m)), |X I k| ≤ A) (β : ℕ) (u : LeftStr L) : |bandArrayL lay X β u| ≤ A

A nonnegative bound A on the absolute values of all entries of X also bounds every value of its left band arrays, for every band index. Zero padding and unused strings are included; 0 ≤ A remains required when N = 0.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_bandArrayR_le {L m N : ℕ} (lay : Layout L m) {Y : Matrix (Fin (D m)) (Fin N) ℤ} {B : ℤ} (hB : 0 ≤ B) (hY : ∀ (k : Fin (D m)) (J : Fin N), |Y k J| ≤ B) (β : ℕ) (v : RightStr L) : |bandArrayR lay Y β v| ≤ B

A nonnegative bound B on the absolute values of all entries of Y also bounds every value of its right band arrays, for every band index. Zero padding and unused strings are included; 0 ≤ B remains required when N = 0.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_encodeWith_le {α : Type} [Fintype α] {c : Term → α → ℤ} (hc : ∀ (lam : Term) (s : α), |c lam s| ≤ 1) {L : ℕ} {a : (Fin L → α) → ℤ} {A : ℤ} (ha : ∀ (u : Fin L → α), |a u| ≤ A) (τ : Leaf L) : |encodeWith c τ a| ≤ ↑(Fintype.card (Fin L → α)) * A

If every coefficient has absolute value at most one and every array entry has absolute value at most A, then an encoded value has absolute value at most the array index type's cardinality times A. This bounds the value of the finite sum defining encodeWith.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_encodingL_le {L : ℕ} {a : LeftStr L → ℤ} {A : ℤ} (ha : ∀ (u : LeftStr L), |a u| ≤ A) (τ : Leaf L) : |encodingL a τ| ≤ 7 ^ L * A

An absolute bound A on the left array entries gives the bound 7 ^ L * A on each value of encodingL.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_encodingR_le {L : ℕ} {b : RightStr L → ℤ} {B : ℤ} (hb : ∀ (v : RightStr L), |b v| ≤ B) (τ : Leaf L) : |encodingR b τ| ≤ 7 ^ L * B

An absolute bound B on the right array entries gives the bound 7 ^ L * B on each value of encodingR.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.abs_result_le {n : ℕ} (encA encB : Leaf n → ℤ) (A B : ℤ) (hA : ∀ (τ : Leaf n), |encA τ| ≤ A) (hB : ∀ (τ : Leaf n), |encB τ| ≤ B) (S : Finset (OutStr n)) (w : OutStr n) : |result n encA encB S w| ≤ 10 ^ n * (A * B)

If encA and encB are bounded in absolute value by A and B, every value returned by Pruned.result is bounded by 10 ^ n * (A * B). This holds for every request set S and output string w, including unrequested strings, whose returned value is zero. It bounds the specified mathematical result, not native scratch states or machine word width.

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

Under D m ^ 18 ≤ N, the number 10 ^ (19 * m) of leaf indices is at most N ^ 2.