Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.Width

Sufficient physical width for native wanted-query grouping #

Main definitions #

Main results #

Coordinates and query codes are unsigned. No signed-kernel width adjustment is needed for this routing component. Relating its parameters to a whole 3SUM input remains composition work.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.admissionWidth (L m N Q : ℕ) :
ℕ

Positive sufficient physical width, logarithmic in the explicit original-parameter budget. The program does not read the width or this threshold.

Instances For
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.admissionWidth_pos (L m N Q : ℕ) :
    0 < admissionWidth L m N Q

    The width condition admits positive widths even for zero dimension and empty queries.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.admission_fit {W L m N Q : ℕ} (hW : admissionWidth L m N Q ≤ W) :
    WordRAM.Fits W (wordBudget L m N Q)

    A sufficiently large physical width guarantees the actual numerical fit premise.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.runs_wide {W L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (hW : admissionWidth L m N qs.length ≤ W) :
    WordRAM.InputFits W (input L m qs) ∧ ∃ (y : WordRAM.Data 96), ∃ n ≤ timeBound L m N qs.length, WordRAM.Runs W (program.program codes) (WordRAM.State.init (input L m qs)) { pc := program.size, data := y } n ∧ WordRAM.Executes W (program.program codes) (WordRAM.State.init (input L m qs)) (codeAddress L m N qs.length) (n + 1) ∧ WordRAM.Data.Bounded W y ∧ (∀ (i : Fin qs.length), y.mem (codeAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑(qs.get i).1 ↑(qs.get i).2)) ∧ y.mem (originalAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑i) ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ inputPairs qs) k < t) qs.length) ∧ y.mem (offsetAddress L m N qs.length + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = qs.length ∧ ∀ (a : ℕ), a < inputLimit qs.length ∨ memoryLimit L m N qs.length ≤ a → y.mem a = (WordRAM.State.init (input L m qs)).data.mem a

    Actual initialized runs at every sufficiently wide physical width. The same returned memory holds the original-index permutation, query codes, exact spans and readonly frame.

    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.program_length_le :
    List.length (program.program codes) ≤ 4096

    The code is one finite 96-register program; all data-dependent repetition is in loops.

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

    The native program is uniform across admitted widths.