Complete native shared-band execution

Main results

• BandPreparation.exec: compute both tables and every shared encoding, from real scalar headers and matrix words, restoring the full original input prefix and every outside cell. All setup, copies, loops and encoder calls contribute to the instruction bound.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.snapshot_le_catalogue (L m N : ℕ) : snapshotBase L m N ≤ catalogueBase L m N

The two tables and the protected input all precede the output catalogue.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogue_side_end_le (L m N : ℕ) (side : Bool) : catalogueAddress L m N side (MatrixMultiplication.Schonhage.numBands L m N) 0 ≤ memoryEnd L m N

The one-side catalogue end is within the complete allocation.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bandTime_le (L : ℕ) : bandTime L + 3 ≤ 512 * (L + 1) * 10 ^ L

A coarse uniform bound for one actual shared-band call and its outer loop control.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.execution_time_le (L m N : ℕ) : 16 * L + 49 + (7 * inputEnd m N + 7 + ((6 * L + 16) * 2 ^ L + 14 + ((6 * L + 17) * 2 ^ L + 4 + (MatrixMultiplication.Schonhage.numBands L m N * (bandTime L + 3) + 3 + (MatrixMultiplication.Schonhage.numBands L m N * (bandTime L + 3) + 3 + (7 * inputEnd m N + 7)))))) ≤ timeBound L m N

The sum of the previously proved native component charges fits the generic bound.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec {w L m N : ℕ} (hw : 0 < w) (hm : m ≤ L) (x : WordRAM.Data 96) (hL : x.mem 1 = L) (hm' : x.mem 2 = m) (hN : x.mem 3 = N) (matrix : Bool → ℕ → ℕ → ℤ) (hmat : ∀ (side : Bool), ∀ r < N, ∀ k < MatrixMultiplication.Schonhage.D m, x.mem (matrixOffset m N side r k + 4) = WordRAM.Signed.encode (matrix side r k)) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (side : Bool), ∀ r < N, ∀ k < MatrixMultiplication.Schonhage.D m, |matrix side r k| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin (w + 2) program x y (timeBound L m N) ∧ BandParameters L m N y ∧ (∀ (side : Bool), ∀ β < MatrixMultiplication.Schonhage.numBands L m N, ∀ p < 10 ^ L, y.mem (catalogueAddress L m N side β p) = WordRAM.Signed.encode (catalogueValue L m N side (matrix side) β p)) ∧ (∀ a < 2 ^ L, y.mem (inverseBase L m N + a) = MatrixMultiplication.Schonhage.MaskTable.lookup L m a) ∧ (∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)), y.mem (tableBase L m N + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) ∧ ∀ (b : ℕ), ¬(inputEnd m N ≤ b ∧ b < memoryEnd L m N) → y.mem b = x.mem b

The full fixed native program. The caller supplies only ordinary L,m,N headers and signed matrix words; both tables and every padded/encoded band are computed. Header zero and arbitrary outside memory need not be zero or describe a standalone input list.