Positive original-input width admission for native queried products

Main results

• QueriedProduct.admissionWidth: sufficient physical width, derived only from original scalar dimensions, entry magnitude and request count.
• QueriedProduct.runs_wide: actual initialized product execution at every sufficiently wide admitted width, with guaranteed input fit and no physical-width reads by the code.

The logarithm applies to the explicit original-input magnitude/address envelope. Relating it to a polynomially bounded whole-3SUM input remains separate composition work under #1394.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.admissionWidth (L m N Q A : ℕ) : ℕ

An original-input-derived sufficient physical width, including the existing two-bit native signed-kernel margin. It is not read by the native program.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.admissionWidth_pos (L m N Q A : ℕ) : 0 < admissionWidth L m N Q A

The physical threshold is strictly positive even for empty and zero-magnitude inputs.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.admission_bounds {W L m N Q A : ℕ} (hW : admissionWidth L m N Q A ≤ W) : 0 < W - 2 ∧ magnitudeBound L A < 2 ^ (W - 2 - 1) ∧ WordRAM.Fits W (wordBudget L m N Q)

Mathlib's ceiling logarithm supplies both numerical admission hypotheses.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.runs_wide {W L m N A : ℕ} (hm : m ≤ L) (bits : Bool) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (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) (hbits : bits = true → (∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k) ∧ ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j) (hW : admissionWidth L m N qs.length A ≤ W) : WordRAM.InputFits W (input bits L X Y qs) ∧ ∃ (y : WordRAM.Data 160), ∃ n ≤ timeBound hm qs, WordRAM.Runs W ((program bits).program output) (WordRAM.State.init (input bits L X Y qs)) { pc := (program bits).size, data := y } n ∧ WordRAM.Executes W ((program bits).program output) (WordRAM.State.init (input bits L X Y qs)) (outputBase L m N qs.length) (n + 1) ∧ WordRAM.Data.Bounded W y ∧ (∀ (i : Fin qs.length), y.mem (outputBase L m N qs.length + ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (a : ℕ), ¬(inputEnd m N qs.length ≤ a ∧ a < memoryEnd L m N qs.length) → y.mem a = (WordRAM.State.init (input bits L X Y qs)).data.mem a

Both real input modes run at every sufficiently wide physical width. All product values, the charged halt and complete restored-input/outside frame refer to the same actual run.