Documentation

Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.RawInput

Original raw matrix and coordinate spans #

These readback lemmas use the existing original product input and row-major numbering. The query list is the finite mathematical reading of actual native coordinate words; the adapter copies those words unchanged, and performs no uncharged query decoding operation.

source
def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.decodedQueries {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ) :
List (Fin n × Fin n)

Mathematical reading of an existing interleaved native query block. The modulo is only a total specification; actual producer coordinates are proved in range before using it.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.decodedQueries_length {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ) :
    (decodedQueries hn mem q Q).length = Q

    Decoding retains exactly the original occurrence count.

    source
    theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.decodedQueries_words {m n q Q : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (hcoord : ∀ i < Q, mem (q + 2 * i) < n ∧ mem (q + 2 * i + 1) < n) (a : ℕ) :
    a < 2 * Q → mem (q + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y (decodedQueries hn mem q Q))).data.mem (5 + 2 * (n * MatrixMultiplication.Schonhage.D m) + a)

    Every actual in-range coordinate word reappears unchanged in the ordinary callee input.

    source
    theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.raw_left_words {m n s : ℕ} (mem : ℕ → ℕ) (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)), mem (s + (↑i * MatrixMultiplication.Schonhage.D m + ↑k)) = (X i k).toNat) (a : ℕ) :
    a < n * MatrixMultiplication.Schonhage.D m → mem (s + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + a)

    A native left-matrix span reads exactly as the ordinary product's original raw input.

    source
    theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.raw_right_words {m n t : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (qs : List (Fin n × Fin n)) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (i : Fin n), mem (t + (↑k * n + ↑i)) = (Y k i).toNat) (a : ℕ) :
    a < n * MatrixMultiplication.Schonhage.D m → mem (t + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + n * MatrixMultiplication.Schonhage.D m + a)

    The right original block retains its D×n row-major order.