Bounds for guarded band addressing

Main results

• bandSize_le_seven_pow: a complete band fits within the tensor input dimension.
• band_position_bounds: all padded row/column arithmetic stays below N+7^L before the native guard. Row-major matrix addresses are computed only after that guard.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandSize_le_seven_pow (L m : ℕ) : bandSize L m ≤ 7 ^ L

The entire band dimension is bounded by the flat tensor input dimension.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.band_position_bounds {L m N β q o : ℕ} (hβ : β < numBands L m N) (hq : q < K0 L m) (ho : o < N0 L m) : β * K0 L m < N + 7 ^ L ∧ β * K0 L m + q < N + 7 ^ L ∧ (β * K0 L m + q) * N0 L m < N + 7 ^ L ∧ (β * K0 L m + q) * N0 L m + o < N + 7 ^ L

Even the last padded band has small block arithmetic. This bound precedes the r<N guard; it does not assert that a padded row/column is a real matrix position.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.numBands_pos {L m N : ℕ} (hm : m ≤ L) (hN : 0 < N) : 0 < numBands L m N

Nonempty matrices need at least one shared band.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bandSize_mul_D_le_ten_pow {L m : ℕ} (hm : m ≤ L) : bandSize L m * D m ≤ 10 ^ L

A full band's original matrix entries fit within one encoding-sized block. This bound is valid for every m≤L, without the thin-regime specialization.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.matrix_entries_le_band_encodings {L m : ℕ} (hm : m ≤ L) (N : ℕ) : N * D m ≤ numBands L m N * 10 ^ L

All original matrix entries are dominated by the shared band catalogue size; this charges input copying/restoration without a separate thin-regime estimate.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.preparation_shape_le {L m N : ℕ} (hm : m ≤ L) (hN : 0 < N) : 1 + N * D m + 2 ^ L + 2 * numBands L m N * 10 ^ L ≤ 5 * (numBands L m N * 10 ^ L)

For nonempty matrices, table initialization and the original matrix input are all dominated by a constant times the shared encoding entry count.