Deriving producer and tile-kernel admission from original inputs #
Main results #
QueriedProduct.kernel_fits: actual separated tile pointers and bounded fresh epochs fit from the single original numerical allocation envelope.QueriedProduct.magnitude_admissions: the original entry envelope covers shared encodings, every pruned partial sum and the actual raw-word doubling instruction.
No intermediate-state fit contract is part of the final caller's input.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.kernel_fits {w L m N Q a b q o n E : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N Q)) (ha : a ≤ BandPreparation.memoryEnd L m N) (hb : b ≤ BandPreparation.memoryEnd L m N) (hq : q ≤ codeBase L m N Q + Q) (ho : o ≤ outputBase L m N Q) (hn : n ≤ Q) (hE : E ≤ epochBound L m N) :
WordRAM.Fits w (PrunedQuery.kernelBudget L (scratchBase L m N Q) a b q o n E)
The shared original allocation bound admits every computed tile's actual pointer values. Query counts retain occurrences; epoch bounds are established by the caller's loop invariant.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.magnitude_admissions {w L A : ℕ} (hw : 0 < w) (hmag : magnitudeBound L A < 2 ^ (w - 1)) :
All signed and conversion admission follows from the original integer-entry magnitude. The extra two physical bits are the existing native signed-kernel convention.