Initialized flat native queried products #
Main results #
QueriedProduct.runs: actualState.initexecutions, exact original-order product values, guaranteed input fit, complete frame and a charged halt tied to the same final memory.QueriedProduct.bounded_reachable: every initialized reachable prefix has fitting data words.QueriedProduct.program_length_le: one fixed finite 160-register program for each input mode.
The code is independent of all dimensions, entry magnitudes, query counts and word widths. These results are component results; they do not instantiate a complete Exact Triangle solver or the ordinary-3SUM endpoint under #1394.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.program_length_le (bits : Bool) :
The full flattened instruction list, including halt, is fixed independently of the input.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.not_readsWidth (bits : Bool) :
¬(program bits).ReadsWidth
Neither mode reads the physical width; the same fixed code runs at every admitted width.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.runs {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) (hbits :
bits = true →
(∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k) ∧ ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j) (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) ∧ ∃ (y : WordRAM.Data 160),
∃ n ≤ timeBound hm qs,
WordRAM.Runs (w + 2) ((program bits).program output) (WordRAM.State.init (input bits L X Y qs))
{ pc := (program bits).size, data := y } n ∧ WordRAM.Executes (w + 2) ((program bits).program output) (WordRAM.State.init (input bits L X Y qs))
(outputBase L m N qs.length) (n + 1) ∧ WordRAM.Data.Bounded (w + 2) y ∧ (∀ (i : Fin qs.length),
y.mem (outputBase L m N qs.length + ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (a : ℕ),
¬(inputEnd m N qs.length ≤ a ∧ a < memoryEnd L m N qs.length) →
y.mem a = (WordRAM.State.init (input bits L X Y qs)).data.mem a
Original matrices and coordinates initialize the real native run. The charged prefix reaches the same memory that contains all product values, and its next instruction halts.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bounded_reachable {w L m N A n : ℕ} (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)) {y : WordRAM.State 160} (hy : WordRAM.Runs (w + 2) ((program bits).program output) (WordRAM.State.init (input bits L X Y qs)) y n) :
WordRAM.Data.Bounded (w + 2) y.data
Every reachable initialized prefix is bounded at the same physical width.