Quantitative saving for actual native queried products #
Main results #
QueriedProduct.thin_timeBound: the native charge, including halt, has the proved thin saving plus an explicit term for every original query occurrence.QueriedProduct.thin_timeBound_sparse: an occurrence-count sparsity condition absorbs that term and gives the complete chargedN² / D^(1/18)bound, with a depth factor.
These results compose the actual native charge with the existing finite encoding/tile/leaf bounds from [AlmanWilliams2026, Section 2]. The occurrence hypothesis in the second result is stronger than the source's distinct-position cardinality condition when requests repeat. No sparse solver or running-time assertion is assumed.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.thin_timeBound (m N : ℕ) (qs : List (Fin N × Fin N)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hW : qs.toFinset.card * 2 ^ m ≤ N ^ 2) :
The source's distinct-position sparsity condition retains an explicit charge for list multiplicity. Every actual copy, conversion, producer, tile, epoch and report is included.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.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) :
A bound on all original occurrences, rather than only distinct coordinates, absorbs the actual list-input/reporting charge. The final halt is included.