Sufficient physical width from original pruned-query inputs

Main definitions

• PrunedQuery.admissionWidth: three bits beyond the binary ceiling logarithm of the combined original magnitude and address budgets.

Main results

• PrunedQuery.runs_wide: at every admitted physical width, the same finite program starts from actual initialized input, returns every requested result and halts within the charged bound.

Input fit is a conclusion, including both scalar headers and the machine's length word. This component's threshold is logarithmic in its explicit budgets. Relating the encoding depth, query count and magnitudes to a whole 3SUM input is separate composition work under #1394.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.admissionWidth (L Q A B : ℕ) : ℕ

A positive threshold for the physical target width, computed from original parameters. The code does not inspect this number or the machine width.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.admissionWidth_pos (L Q A B : ℕ) : 0 < admissionWidth L Q A B

The physical threshold is nonzero even for empty inputs and zero operands.

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

Mathlib's ceiling logarithm derives both actual address-word fit and the signed source envelope, retaining the two extra bits charged by the existing signed arithmetic kernels.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.runs_wide {W L A B : ℕ} (a b : Fin (10 ^ L) → ℤ) (qs : List (Fin (10 ^ L))) (ha : ∀ (v : Fin (10 ^ L)), |a v| ≤ ↑A) (hb : ∀ (v : Fin (10 ^ L)), |b v| ≤ ↑B) (hW : admissionWidth L qs.length A B ≤ W) : WordRAM.InputFits W (input L a b qs) ∧ ∃ (y : WordRAM.Data registers), ∃ n ≤ timeBound qs, WordRAM.Runs W (program.program output) (WordRAM.State.init (input L a b qs)) { pc := program.size, data := y } n ∧ WordRAM.Executes W (program.program output) (WordRAM.State.init (input L a b qs)) (outputBase L qs.length) (n + 1) ∧ WordRAM.Data.Bounded W y ∧ (∀ (i : Fin qs.length), y.mem (outputBase L qs.length + ↑i) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.Pruned.result L (fun (v : MatrixMultiplication.Schonhage.Leaf L) => a (Encoding.leafIndex v)) (fun (v : MatrixMultiplication.Schonhage.Leaf L) => b (Encoding.leafIndex v)) (requested qs) (queryAt (qs.get i)))) ∧ ∀ (c : ℕ), ¬(outputBase L qs.length ≤ c ∧ c < memoryEnd L qs.length) → y.mem c = (WordRAM.State.init (input L a b qs)).data.mem c

A complete initialized run at every sufficiently wide physical width, with guaranteed input fit, a shared pre-halt memory witness, charged halt, all output values and outside preservation.