Original matrix and coordinate inputs for queried products

Main definitions

• QueriedProduct.entryWord: canonical signed words or original raw nonnegative words.
• QueriedProduct.input: four scalar headers, both row-major matrices and raw coordinates.

The raw-input program performs actual doubling before calling the signed producer. In particular, raw 0/1 entries become canonical signed 0/2 words. This input definition neither supplies encodings nor performs that target conversion on the caller's behalf.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.entryWord (bits : Bool) (z : ℤ) : ℕ

Ordinary source words. In raw mode only nonnegative source values are represented; the native matrix-copy loop performs the subsequent signed-encoding conversion.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.convert_entryWord (bits : Bool) (z : ℤ) (hz : bits = true → 0 ≤ z) : (if bits = true then 2 * entryWord bits z else entryWord bits z) = WordRAM.Signed.encode z

Actual doubling converts every nonnegative raw entry into its canonical signed word. In particular, the raw unsigned zero/one producer convention becomes signed zero/two.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.matrixInput {m N : ℕ} (bits : Bool) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) : List ℕ

Both original matrices in their ordinary row-major input order.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input {m N : ℕ} (bits : Bool) (L : ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) : List ℕ

Actual initialized input, using exactly the existing router's raw coordinate convention.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.matrixInput_length {m N : ℕ} (bits : Bool) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) : (matrixInput bits X Y).length = 2 * (N * MatrixMultiplication.Schonhage.D m)

The matrix block contains exactly both original input arrays.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input_length {m N : ℕ} (bits : Bool) (L : ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) : (input bits L X Y qs).length + 1 = inputEnd m N qs.length

Every original scalar, matrix entry and coordinate lies within the snapshot prefix.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input_query_word {m N : ℕ} (bits : Bool) (L : ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (i : Fin qs.length) (s : Fin 2) : (WordRAM.State.init (input bits L X Y qs)).data.mem (queryInputBase m N + 2 * ↑i + ↑s) = if s = 0 then ↑(qs.get i).1 else ↑(qs.get i).2

The complete initialized input retains the router's raw coordinate values; the matrices only shift their original address. No query code or tile is supplied in these words.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input_matrix_word {L m N : ℕ} (bits : Bool) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (side : Bool) (r k : ℕ) (hr : r < N) (hk : k < MatrixMultiplication.Schonhage.D m) : (WordRAM.State.init (input bits L X Y qs)).data.mem (BandPreparation.matrixOffset m N side r k + 5) = entryWord bits (BandPreparation.matrixValues X Y side r k)

Both original row-major matrix blocks contain precisely their supplied entry words, before any copying, sign conversion or encoding takes place.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.entryWord_fits {w L A : ℕ} (hw : 0 < w) (bits : Bool) (z : ℤ) (hz : |z| ≤ ↑A) (hmag : magnitudeBound L A < 2 ^ (w - 1)) : WordRAM.Fits (w + 2) (entryWord bits z)

The original magnitude envelope covers both canonical signed and raw unsigned words. Raw-word fit does not itself assert nonnegativity of the represented source entries; that extra semantic premise is used by the actual conversion proof.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input_fits {w L m N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (bits : Bool) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (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 : magnitudeBound L A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N qs.length)) : WordRAM.InputFits (w + 2) (input bits L X Y qs)

Every actual initialized word fits from original dimensions and entry magnitudes. No intermediate machine-state fit certificate is supplied.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.input_raw_matrix_le {L m N A : ℕ} (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (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) (j : ℕ) (hj : j < 2 * (N * MatrixMultiplication.Schonhage.D m)) : (WordRAM.State.init (input true L X Y qs)).data.mem (5 + j) ≤ A

Original raw matrix words are bounded by the original absolute-entry bound, at every flat position. This supplies the actual conversion loop without an intermediate fit premise.