Actual all-tile execution with shared encodings and epochs

Main definitions

• QueriedProduct.tileCharge: the charge of one actual tile call and its outer loop control.

Main results

• QueriedProduct.exec_evaluateTiles: every original request receives its exact matrix-product value in grouped order, while actual returned epochs retain one shared timestamp directory.

The finite charge uses original coordinate occurrences and the existing pruned trace count. The proof derives it from executed spans and calls. No sparse bound is assumed.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.tileCharge {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (t : ℕ) : ℕ

Per-tile analysis of the actual program, including call setup, returned epoch/index updates and two outer-loop instructions. Duplicate coordinate occurrences remain charged.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_evaluateTiles {w L m N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (x : WordRAM.Data 160) (hp : Parameters L m N qs.length x) (hi : x.regs index = 0) (hE : x.regs epoch = 0) (hg : SavedGroups L m N qs.length old x.mem) (he : EncodedBands hm X Y x.mem) (hvalues : ∀ (i : Fin qs.length), old (Wanted.codeAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.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, old (Wanted.offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < t) qs.length) (hmarks : ∀ j < 10 ^ L, x.mem (stampBase L m N qs.length + j) = 0) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ ↑A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ ↑A) (hmag : magnitudeBound L A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N qs.length)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin (w + 2) evaluateTiles x y (∑ t ∈ Finset.range (MatrixMultiplication.Schonhage.numBands L m N ^ 2), tileCharge hm qs t + 2) ∧ Parameters L m N qs.length y ∧ SavedGroups L m N qs.length old y.mem ∧ EncodedBands hm X Y y.mem ∧ (∀ (i : Fin qs.length), y.mem (groupedBase L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (p : ℕ), ¬(groupedBase L m N qs.length ≤ p ∧ p < outputBase L m N qs.length) → ¬(scratchBase L m N qs.length ≤ p ∧ p < memoryEnd L m N qs.length) → y.mem p = x.mem p

Every real tile is evaluated by the same fixed program. The zero-band case exits without division, and repeated requested coordinates retain their distinct grouped positions.