Initialized runs with the finite wanted-set interface #
Main results #
Wanted.runs_grouped: one actual initialized native run computes each tile's query-code span and a permutation retaining all original positions, within the charged bound.
This is the routing interface for subsequent shared-band and pruned-kernel composition.
It does not evaluate the product or reconstruct answers. Stage execution lemmas in the
supporting modules are internal implementation APIs; consumers use this theorem or runs.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.runs_grouped {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 : ℕ),
n + 1 ≤ 128 * (L + 1) * (qs.length + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 2 ^ L + 1) ∧ 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.tiles L m N,
Finset.image (fun (j : ℕ) => y.mem (codeAddress L m N qs.length + j))
(Finset.Ico
(y.mem
(offsetAddress L m N qs.length + (T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2)))
(y.mem
(offsetAddress L m N qs.length + (T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2 + 1)))) = Finset.image (fun (w : MatrixMultiplication.Schonhage.OutStr L) => ↑(PrunedQuery.queryIndex w))
(MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm)
qs.toFinset T.1 T.2)) ∧ (∀ j < qs.length, y.mem (codeAddress L m N qs.length + j) < 10 ^ L) ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (offsetAddress L m N qs.length + t) ≤ y.mem (offsetAddress L m N qs.length + (t + 1)) ∧ y.mem (offsetAddress L m N qs.length + (t + 1)) ≤ qs.length) ∧ (∀ j < qs.length, y.mem (originalAddress L m N qs.length + j) < qs.length) ∧ (Function.Injective fun (j : Fin qs.length) => y.mem (originalAddress L m N qs.length + ↑j)) ∧ Finset.image (fun (j : ℕ) => y.mem (originalAddress L m N qs.length + j))
(Finset.range qs.length) = Finset.range 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 native grouping from the original raw coordinate list at every sufficiently wide physical width. The same final memory supplies the tile spans, permutation and frame. No layout, query-code, count or permutation certificate is supplied as input.