Source-regime logarithmic width for actual queried products

Main results

• QueriedProduct.thin_envelopes: original dimensions give polynomial magnitude/address envelopes and an explicit polynomial allocation bound.
• QueriedProduct.thin_admissionWidth_le: a positive constant times the logarithm of original dimension, request count and entry magnitude suffices in the source's thin regime.

These bounds concern the real native program and its actual allocation formulas. They assume neither intermediate-state fits nor a polynomial-space certificate.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.thin_envelopes (m N Q A : ℕ) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) : magnitudeBound (19 * m) A + wordBudget (19 * m) m N Q + 1 ≤ 2 ^ 40 * (N + Q + A + 2) ^ 10 ∧ memoryEnd (19 * m) m N Q ≤ 128 * (N + Q + A + 2) ^ 4

The source regime controls every original power, computed band count and address term. The deliberately loose integer constants leave a uniform logarithmic-width margin.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.thin_admissionWidth_le (m N Q A : ℕ) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) : admissionWidth (19 * m) m N Q A ≤ 128 * Nat.clog 2 (N + Q + A + 2)

A fixed positive logarithmic-width coefficient suffices throughout the thin regime.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.runs_thin {W m N A : ℕ} (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)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hQ : qs.length * 2 ^ m ≤ N ^ 2) (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 : 128 * Nat.clog 2 (N + qs.length + A + 2) ≤ W) : WordRAM.InputFits W (input bits (19 * m) X Y qs) ∧ ∃ (y : WordRAM.Data 160) (n : ℕ), WordRAM.Runs W ((program bits).program output) (WordRAM.State.init (input bits (19 * m) X Y qs)) { pc := (program bits).size, data := y } n ∧ WordRAM.Executes W ((program bits).program output) (WordRAM.State.init (input bits (19 * m) X Y qs)) (outputBase (19 * m) m N qs.length) (n + 1) ∧ ↑(n + 1) ≤ 4325376 * ↑(19 * m + 1) * ↑N ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18) ∧ WordRAM.Data.Bounded W y ∧ (∀ (i : Fin qs.length), y.mem (outputBase (19 * m) 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 (19 * m) m N qs.length) → y.mem a = (WordRAM.State.init (input bits (19 * m) X Y qs)).data.mem a

Complete initialized native thin-product execution at a fixed positive logarithmic-width threshold. Every original occurrence is answered, including duplicates, and halt is charged. The occurrence-count condition is stated explicitly rather than replaced by set cardinality.