Original-parameter width, space and charge for callable products

The virtual window reservation is polynomial in the original row and occurrence counts. Its large fixed exponent is explicit; the program does not initialize that whole interval. Actual setup and return work is linear in original matrix/input size, plus the translated product. Distinct-set sparsity retains the additive occurrence charge; occurrence sparsity absorbs it.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.windowSize_le (N Q : ℕ) : windowSize N Q ≤ (2 * (N + Q + 3)) ^ 128

The reserved window has a fixed polynomial size in original dimensions and query count.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.physical_fits {W b N Q : ℕ} (hW : 256 * Nat.clog 2 (b + N + Q + 5) ≤ W) : WordRAM.Fits W (b + 4 * windowSize N Q + 1024)

Every physical width at least a positive logarithmic threshold admits the complete runtime window and all setup/return addresses. No intermediate-fit certificate is needed.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.timeBound_le {m N : ℕ} (qs : List (Fin N × Fin N)) : timeBound qs + 3 ≤ 3 * (QueriedProduct.timeBound ⋯ qs + 1) + 2048 * (N * MatrixMultiplication.Schonhage.D m + qs.length + 1)

Full standalone charge (including its base load and halt): constant-factor actual product cost plus linear adaptation. No bulk-window or caller-catalogue copy is hidden in this bound.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.thin_timeBound {m N : ℕ} (qs : List (Fin N × Fin N)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hQ : qs.toFinset.card * 2 ^ m ≤ N ^ 2) : ↑(timeBound qs + 3) ≤ 262144 * ↑(19 * m + 1) * (65 * (↑(MatrixMultiplication.Schonhage.D m) ^ (-(1 / 18)) * ↑N ^ 2) + ↑qs.length)

Under distinct-position sparsity, every duplicate occurrence retains its additive charge. This quantitative saving bounds the real callable program, including initialization and halt.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.thin_timeBound_sparse {m N : ℕ} (qs : List (Fin N × Fin N)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hQ : qs.length * 2 ^ m ≤ N ^ 2) : ↑(timeBound qs + 3) ≤ 17301504 * ↑(19 * m + 1) * ↑N ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18)

Occurrence sparsity absorbs the duplicate charge and yields the complete charged saving.