Actual initialized-input execution of native pruned queries

Main definitions

• PrunedQuery.timeBound: the full charged prefix, including setup and duplicate reporting.

Main results

• PrunedQuery.exec_input: the fixed program starts at State.init, computes the existing finite pruned values, preserves the input and outside memory, and leaves bounded native words.

The input contains ordinary depth/count headers, two canonical signed arrays and query codes. All child lists and directories are computed. No layout, execution or timing certificate is an input word or an admission hypothesis.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.timeBound {L : ℕ} (qs : List (Fin (10 ^ L))) : ℕ

Full prefix charge: actual header/power/pointer work, root deduplication, every recursive controller instruction, loop exit and reporting in the original supplied order.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.timeBound_add_one_le {L : ℕ} (qs : List (Fin (10 ^ L))) : timeBound qs + 1 ≤ 8192 * (L + qs.length + 1 + (L + 1) * (MatrixMultiplication.Schonhage.leaves (requested qs)).card)

Pruning gives a bound in terms of the actual contributing leaf set, retaining the setup and duplicate-query costs. This includes one additional final halt instruction.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.input_fits {w L A B : ℕ} (hw : 0 < w) (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) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L qs.length)) : WordRAM.InputFits (w + 2) (input L a b qs)

Both scalar headers, both signed arrays, all query codes and the machine's unsigned length header fit the same admitted target width.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_input {w L A B : ℕ} (hw : 0 < w) (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) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L qs.length)) : WordRAM.InputFits (w + 2) (input L a b qs) ∧ ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin (w + 2) program (WordRAM.State.init (input L a b qs)).data y (timeBound qs) ∧ WordRAM.Data.Bounded (w + 2) 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) ∧ y.regs output = outputBase L qs.length

Execution of the complete native program on actual initialized memory. The final memory witness is shared by execution, mathematical outputs, frame preservation and boundedness.