Composing the actual copied spans with the original product input

The local input meaning uses the unchanged queried-product State.init convention. Matrix and coordinate readback is separated by the three actual source spans; no encoded bands, routing data or precomputed execution contract is present in these assertions.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.original_header {m n : ℕ} (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (qs : List (Fin n × Fin n)) : { base := 0, length := 5 }.Realizes (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem ![4 + 2 * (n * MatrixMultiplication.Schonhage.D m) + 2 * qs.length, 19 * m, m, n, qs.length]

The original product's first five memory words, including its actual payload length.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.local_input {m n b : ℕ} (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (qs : List (Fin n × Fin n)) (mem : ℕ → ℕ) (hhead : { base := b, length := 5 }.Realizes mem ![4 + 2 * (n * MatrixMultiplication.Schonhage.D m) + 2 * qs.length, 19 * m, m, n, qs.length]) (hleft : ∀ a < n * MatrixMultiplication.Schonhage.D m, mem (b + 5 + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + a)) (hright : ∀ a < n * MatrixMultiplication.Schonhage.D m, mem (b + 5 + n * MatrixMultiplication.Schonhage.D m + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + n * MatrixMultiplication.Schonhage.D m + a)) (hqueries : ∀ a < 2 * qs.length, mem (b + 5 + 2 * (n * MatrixMultiplication.Schonhage.D m) + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + 2 * (n * MatrixMultiplication.Schonhage.D m) + a)) (a : ℕ) : a < MatrixMultiplication.Schonhage.QueriedProduct.inputEnd m n qs.length → mem (b + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem a

Exact readback of the five header words and three copied spans identifies the entire unchanged original input. This is a pure consequence of those native stores and copies.