Complete native callable queried-product execution

The caller supplies original zero/one matrices and coordinate occurrences in a local original input block. The product computes its own tables, layouts, groups, encoded bands, epochs and answers. Every source memory access is translated to actual base addition and load/store code; dirty words are normalized without bulk clearing. The final answer pointer is absolute.

This is the callable product prerequisite for an ET-record adapter, not that adapter, an Exact Triangle solver or the complete ordinary-3SUM bound under #1394.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.timeBound {m N : ℕ} (qs : List (Fin N × Fin N)) : ℕ

The complete charge includes two linear span normalizations and the computed setup.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.exec {W b m N : ℕ} (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (x : WordRAM.Data 163) (hb : x.regs Reg.base = b) (hinput : ∀ a < QueriedProduct.inputEnd m N qs.length, x.mem (b + a) = (WordRAM.State.init (QueriedProduct.input true (19 * m) X Y qs)).data.mem a) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j ∧ Y k j ≤ 1) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hfit : WordRAM.Fits W (b + 4 * windowSize N qs.length + 1024)) : ∃ (y : WordRAM.Data 163), WordRAM.ExecWithin W program x y (timeBound qs) ∧ y.regs Reg.result = b + QueriedProduct.outputBase (19 * m) m N qs.length ∧ y.regs Reg.base = b ∧ y.regs Reg.modulus = windowSize N qs.length ∧ (∀ (i : Fin qs.length), y.mem (b + (QueriedProduct.outputBase (19 * m) m N qs.length + ↑i)) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ (∀ a < QueriedProduct.inputEnd m N qs.length, y.mem (b + a) = x.mem (b + a)) ∧ ∀ (a : ℕ), a < b ∨ b + windowSize N qs.length ≤ a → y.mem a = x.mem a

Caller-safe actual native product execution. The only local memory premise is the original input block; all remaining target memory may be dirty. Every original occurrence is answered exactly, original input words are restored exactly, and the caller memory outside the window is preserved. The numerical width hypothesis is derived from original dimensions and base.