Flat native preparation of every public band encoding

Main results

• BandPreparation.runs: actual flat State.init run, all public left/right encodings for the computed deterministic layout, retained computed tables, input/outside frame and charged halt.
• BandPreparation.program_length_le: one fixed finite program, independent of every parameter.

This is a bounded preparation component under the ordinary native 3SUM objective, not a whole 3SUM algorithm or a pruned-query evaluation theorem.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogueValue_left {L m N : ℕ} (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (matrix : ℕ → ℕ → ℤ) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), matrix ↑i ↑k = X i k) (β : ℕ) (τ : MatrixMultiplication.Schonhage.Leaf L) : catalogueValue L m N false matrix β ↑(Encoding.leafIndex τ) = MatrixMultiplication.Schonhage.encodingL (MatrixMultiplication.Schonhage.bandArrayL (MatrixMultiplication.Schonhage.MaskTable.layout hm) X β) τ

The left catalogue retains the original mathematical band and leaf interfaces.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogueValue_right {L m N : ℕ} (hm : m ≤ L) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (matrix : ℕ → ℕ → ℤ) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (i : Fin N), matrix ↑i ↑k = Y k i) (β : ℕ) (τ : MatrixMultiplication.Schonhage.Leaf L) : catalogueValue L m N true matrix β ↑(Encoding.leafIndex τ) = MatrixMultiplication.Schonhage.encodingR (MatrixMultiplication.Schonhage.bandArrayR (MatrixMultiplication.Schonhage.MaskTable.layout hm) Y β) τ

The right catalogue uses the same original flat leaf order.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.program_length_le : List.length (program.program catalogue) ≤ 16384

One finite code-size bound for the 96-register program and its final halt.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.not_readsWidth : ¬program.ReadsWidth

The uniform program does not inspect its target word width.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.runs {w L m N : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (A : ℤ) (hA : 0 ≤ A) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N)) : WordRAM.InputFits (w + 2) (input L m N X Y) ∧ ∃ (y : WordRAM.Data 96), ∃ n ≤ timeBound L m N, WordRAM.Runs (w + 2) (program.program catalogue) (WordRAM.State.init (input L m N X Y)) { pc := program.size, data := y } n ∧ WordRAM.Executes (w + 2) (program.program catalogue) (WordRAM.State.init (input L m N X Y)) (catalogueBase L m N) (n + 1) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ β < MatrixMultiplication.Schonhage.numBands L m N, ∀ (τ : MatrixMultiplication.Schonhage.Leaf L), y.mem (catalogueAddress L m N false β ↑(Encoding.leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingL (MatrixMultiplication.Schonhage.bandArrayL (MatrixMultiplication.Schonhage.MaskTable.layout hm) X β) τ)) ∧ (∀ β < MatrixMultiplication.Schonhage.numBands L m N, ∀ (τ : MatrixMultiplication.Schonhage.Leaf L), y.mem (catalogueAddress L m N true β ↑(Encoding.leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingR (MatrixMultiplication.Schonhage.bandArrayR (MatrixMultiplication.Schonhage.MaskTable.layout hm) Y β) τ)) ∧ (∀ 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 = (WordRAM.State.init (input L m N X Y)).data.mem b

Every row and column band is encoded exactly once into its shared flat block. The actual input contains only the three scalar parameters and signed matrices. w is the signed source magnitude width and w+2 is the target width used by the existing native kernels. The prefix run exposes the actual final memory; its next instruction is the charged halt. No unrelated caller memory or header is required to be zero in the general exec theorem.