Consumer meaning of the computed query groups #
Main results #
Wanted.code_span_eq_wantedStrings: the actual stored offsets select exactly the original finitewantedStringscodes of each tile.Wanted.originals_permutation: the actual original-position words form a permutation, retaining all occurrences, including duplicate pairs.
These representation lemmas consume the memory equations returned by the initialized run. They neither replace the native grouping code nor supply any input certificate to it.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tileKey_eq_iff {L m N : ℕ} (hm : m ≤ L) (i j : Fin N) (T : ℕ × ℕ) (hT : T ∈ MatrixMultiplication.Schonhage.tiles L m N) :
tileKey L m N (↑i, ↑j) = T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2 ↔ MatrixMultiplication.Schonhage.bandOf L m ↑i = T.1 ∧ MatrixMultiplication.Schonhage.bandOf L m ↑j = T.2
An in-range tile key identifies exactly the original row and column bands.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.code_span_eq_wantedStrings {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (μ : ℕ → ℕ) (T : ℕ × ℕ) (hT : T ∈ MatrixMultiplication.Schonhage.tiles L m N) (hvalues :
∀ (i : Fin qs.length),
μ (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))) (hoffsets :
∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2,
μ (offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ inputPairs qs) k < t) qs.length) :
Finset.image (fun (j : ℕ) => μ (codeAddress L m N qs.length + j))
(Finset.Ico (μ (offsetAddress L m N qs.length + (T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2)))
(μ (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)
A tile's actual stored half-open span contains exactly the existing mathematical
wantedStrings codes. Duplicate list occurrences have the same set meaning and are
retained separately by the original-position permutation.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.originals_permutation {L m N : ℕ} (qs : List (Fin N × Fin N)) (μ : ℕ → ℕ) (h :
∀ (i : Fin qs.length),
μ (originalAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑i) :
(∀ j < qs.length, μ (originalAddress L m N qs.length + j) < qs.length) ∧ (Function.Injective fun (j : Fin qs.length) => μ (originalAddress L m N qs.length + ↑j)) ∧ Finset.image (fun (j : ℕ) => μ (originalAddress L m N qs.length + j)) (Finset.range qs.length) = Finset.range qs.length
The actual stored original indices are in range, injective, and cover every input position. Equal original coordinate pairs therefore retain their separate occurrences.